Stream: Miscellaneous

Topic: Matita

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?

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

Enrico Tassi (Apr 03 2023 at 11:57):

Ideas from Matita which made it into Coq:

• bidirectionality hints for the pretyper
• reverse coercions (non-uniform coercions in Matita's slang)

Cross fertilization:

• SSReflect contextual patterns --- Matita's textual representation of a subterm selection made with the mouse
• Irrelevant arguments in conversion --- definitional irrelevance in SProp (maybe unconcious)

In the works:

• Matita's macros - LSP quickfix (more general, but will allow to implement the macros we had in Matita)
• Unification Hints in Matita - elaborator written in Coq-Elpi

Same mistakes:

• UI based on OCaml + GTK

Still good in Matita:

• toplevel (named) fixpoints --- discontinued attempt in Coq
• superposition prover (applyS, equality chains)
• program/russell mode integrated in the pretyper (no special mode)

Never understood which is better:

• pure DeBruijn (Matita) --- locally nameless (Coq)

Outdated tech, don't use:

• mathML

Karl Palmskog (Apr 03 2023 at 12:07):

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

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).

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

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.

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.

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: Nov 29 2023 at 21:01 UTC