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?

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

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

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

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.

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…

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 think Matita is considered quite simple, at least compared to Coq? It's CIC: http://matita.cs.unibo.it / https://github.com/LPCIC/matita

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: Jun 23 2024 at 05:02 UTC