@nprofile1q... what @nprofile1q... tells us is that, if we want to teach programming concepts and design, we ought to use a teaching language. (He'll correct my butchering, so I'm happy to butcher his quote.)
I don't see why we shouldn't have teaching provers, apart from the fact that we're still in the craft stage of prover construction.

@nprofile1q... @nprofile1q...