It's Meta Language. The ML language was developed in the early 1970s as a meta-l...

more_original on Jan 1, 2017 | parent | context | favorite | on: CakeML – A Verified Implementation of ML

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)

jez on Jan 2, 2017 [–]

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