It’s been decades since I could claim to know anything about this field so I’m probably completely wrong in how I read this, but the idea that one might build a theorem prover (“ML!”) for one’s non-ML programming language and have the prover itself accidentally be a really good general purpose programming language … is very funny.