4 ms·

> A proof checker meant for education What makes it for education? Why can't it be used as a general purpose proof checker?

• Jtsummers 2y ago
  It doesn't seem as full-featured as other systems at this point. For instance, there doesn't seem to be code generation to go from the proven code to another language (like Rocq, formerly Coq, and others can do).
• proof_by_vibes 2y ago
  I would argue there is merit in keeping a platform separate for the purpose of education. Humans shape their tools that in turn shape themselves. In a general purpose theorem proving environment, such as with Lean, there is a different attitude about what level of abstraction to expose by default. It's less intuitive to a child to have a tutor need to explain what it means for a function to be `unsafe` than it is to explain what it means to `print` an expression. By creating a separate platform, you can set these defaults to curate different kinds of engagement with users. Take the `processing` language as an example. While it's Java under the hood, the careful curation of the programming environment incentivizes learners to play with it like a toy, increasing creative expression and fault-less experimentation.
  • fc417fc802 2y ago
    I agree but it's interesting to observe that occasionally a work can morph. Racket is a good example. Initially an academic toy, these days it performs quite well and has an expansive ecosystem.
• YetAnotherNick 2y ago
  Having worked a little bit in Lean and Agda(which is also educational-ish), Lean has all sorts of magical convenience features. For educational proof checker, I think it would be good to be more clear about things and being more mechanical, have a smaller kernel with lower expressivity of types(have strong normalization, don't have universe polymorphism, Large elimination etc).