Stream: Miscellaneous

Topic: Matita


view this post on Zulip Patrick Nicodemus (Apr 02 2023 at 00:19):

It seems that Matita is retired from active development now. All links to it online are dead.
I have read one or two of the papers on the main philosophy and development of the software and I was curious, for anyone that has used it or participated in its development, what the main takeaways from it are? What worked, what did not? Are there any ideas which were implemented in Matita (and its editor) or scheduled for Matita which can be or should be implemented in Coq and coq-lsp, such as tinycals?

view this post on Zulip Emilio Jesús Gallego Arias (Apr 02 2023 at 21:22):

Hi @Patrick Nicodemus , I think the main matita expert around here is @Enrico Tassi , I'll let him answer to your questions but based on my understanding, Matita had many good ideas that could be useful for Coq

view this post on Zulip Enrico Tassi (Apr 03 2023 at 11:57):

Ideas from Matita which made it into Coq:

Cross fertilization:

In the works:

Same mistakes:

Still good in Matita:

Never understood which is better:

Outdated tech, don't use:

view this post on Zulip Karl Palmskog (Apr 03 2023 at 12:07):

I thought Matita helped clarify the unification hints vs. canonical structures vs. typeclass inference thing?

view this post on Zulip Enrico Tassi (Apr 03 2023 at 12:31):

Well, my take away was that with the looking glasses of logic programming they are all the same mechanism, hence Elpi, a language to express these. Coq-Elpi did serve other purposes so far, but I finally got to the point where we (a student of mine and me) started to implement type class search with it. So my original plan of unifying these mechanisms begins to see the light (finally).

view this post on Zulip Paolo Giarrusso (Apr 03 2023 at 21:22):

I know a lot of iris users are also looking forward to an opt-in "unifall-the-resurrected" — which seems implied from the goal

view this post on Zulip Claudio Sacerdoti Coen (Apr 07 2023 at 17:05):

Btw, due to the advent of ocaml 5, I took some time to port Matita to recent compilation technology (opam/dune/...).
The code is now hosted on Github https://github.com/sacerdot/ and it is now easy to install it (just clone + opam pin).
It is still used in Bologna for didatics (it has a declarative language used for that) and for some formalizations.

view this post on Zulip Enrico Tassi (Apr 07 2023 at 18:32):

@Claudio Sacerdoti Coen I'd be more than happy to hear your thoughts about what Matita did well. I'm pretty sure my view on the web technology is very partial, for example.

view this post on Zulip Patrick Nicodemus (Apr 07 2023 at 19:26):

A 2012 paper on "User interaction with the Matita Proof Assistant" stresses the "philosophy of library management":

The Matita system is meant to be first of all an interface between the user and the mathematical library; this makes a clear methodological difference between Matita and most of the current tool for the interactive support to formal reasoning, whose emphasis is traditionally on different aspects, such as authoring or proof checking.

Do you think this dream was realized? Do you think that it is still a desirable goal to have a proof assistant which gives a privileged place to fast and easy communication with a large library?


Last updated: Jun 13 2024 at 06:01 UTC