Comment by pfdietz

ML was designed to be the metalanguage for the LCF proof system, used to write proof tactics. It was then recognized to be interesting in its own right as a programming language.