Hacker News new | ask | show | jobs
by more_original 3457 days ago
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)

1 comments

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