Stream: Coq users

Topic: Tiny proof assistant for experiments?

YoungJu Song (Sep 04 2023 at 12:45):

I would like to make some experiments on the kernel side of the proof assistant, and Coq seems too big for this purpose. Is there some tiny proof assistant (that implements CoC or CIC or some other reasonably simple and expressive variant) for experimental purposes?

Karl Palmskog (Sep 04 2023 at 12:48):

there is MetaCoq, but it "only" has the checker part (and term/type language) of what is usually considered a full CoC/CIC proof assistant: https://github.com/MetaCoq/metacoq

Karl Palmskog (Sep 04 2023 at 14:28):

as usual, I also mention Candle which has more proof assistant-like functionality but for simple types (HOL)

Gaëtan Gilbert (Sep 04 2023 at 14:44):

dedukti isn't COC IIRC but may be close enough depending on what you want to do

Meven Lennon-Bertrand (Sep 04 2023 at 17:22):

There are also many small proofs assistants/type-checkers out there, built either for experimental or pedagogical aims. Let me mention spartan theory, the elaboration zoo, the little typer, Andromeda (2), but there are many more.

Meven Lennon-Bertrand (Sep 04 2023 at 17:24):

Also note that depending on what you are looking for, MetaCoq might not be very well-suited: although its checker is quite simple in principle, it is very much entangled into the complex setup that is necessary for certification, and so I'm not sure it allows for easy experimentation…

Karl Palmskog (Sep 04 2023 at 17:33):

hard to beat HOL Light as a practical/experimentable system with small kernel, even though it's HOL, which may be a deal-breaker here. There is a reason it's a frequent target of "kernel experiments", e.g., for learning

Karl Palmskog (Sep 04 2023 at 17:41):

I think Matita is considered quite simple, at least compared to Coq? It's CIC: http://matita.cs.unibo.it / https://github.com/LPCIC/matita

Meven Lennon-Bertrand (Sep 05 2023 at 08:37):

Karl Palmskog said:

hard to beat HOL Light as a practical/experimentable system with small kernel, even though it's HOL, which may be a deal-breaker here. There is a reason it's a frequent target of "kernel experiments", e.g., for learning

I guess the question is what you want to learn: if you want to play around with any proof assistant kernel, then indeed HOL (Light) is an excellent target (I recall reimplementing a very light version of it in a master course in only a few days). But if you want to play with dependent types, or even a kernel which does not follow the LCF approach, eg which has explicit proof witnesses, then you must go look for something else.

Last updated: Oct 13 2024 at 01:02 UTC