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?
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
Ideas from Matita which made it into Coq:
In the works:
Still good in Matita:
Never understood which is better:
Outdated tech, don't use:
I thought Matita helped clarify the unification hints vs. canonical structures vs. typeclass inference thing?
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).
I know a lot of iris users are also looking forward to an opt-in "unifall-the-resurrected" — which seems implied from the goal
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.
@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.
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: Nov 29 2023 at 21:01 UTC