[Twirrim]

What is ML in this context? Neither CakeML nor Standard ML site appear to actually define it, and it's an acronym with a few definitions in tech (e.g. Machine Learning)

[more_original]

It's Meta Language. The ML language was developed in the early 1970s as a meta-language for the LCF theorem prover. ML was developed as a language for programming proof tactics. The strong type system and type soundness guarantees of ML were important to guarantee that such tactics could only prove correct theorems.

https://en.wikipedia.org/wiki/ML_(programming_language)

[z1mm32m4n]

For a bit of history about ML, see Appendix F: The Development of ML (on page 89) from here:

http://sml-family.org/sml97-defn.pdf

[igravious]

https://en.wikipedia.org/wiki/ML_(programming_language)