[proof_by_vibes]

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]

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.