Yeah, I should have. There's been prior work porting linear types and other stuff (think Rust safety) like that to ML since that's an easy-to-analyze language academics like to work in. Tolmach et al actually made a converter for it to Ada one time. ML is also the language that most formal verification extracts to by default. CakeML is a verified compiler for ML. There's flow analysis and concurrent variants for it. So, ML by itself is a good choice for correct code that will get a lot of analysis. Imperative ML, imperative for the needed efficiency gains, combined with type systems like Rust's to ensure its safety with numbers mapped to say 64-bit can go a long way.
When I wrote it, though, I was mainly thinking of recent work that converts functional, verified specs into imperative specs that extracts to ML. I think that has a lot of potential for producing a pile of verified data structures with low cost similarly to the COGENT language that was used for ext2 filesystem. Got a link for Imperative/HOL-to-ML below.
