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.

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.

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

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