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

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.