Masterminds of Programming

Chapter 9. ML

ML is a general-purpose functional language developed by Robin Milner and the team he led at the University of Edinburgh in the 1970s. It grew from a metalanguage project designed to describe mathematical proofs. ML’s most valuable contribution to language design may be the Hindley-Milner type inference algorithm used in many static, latent type systems. The language inspired Standard ML, Caml, Haskell, and F#, among others.

The Soundness of Theorems

You created LCF, one of the first tools for automated theorem proving, and the programming language ML to run the proving. How did it work?

Robin Milner: There were other efforts at machine-assisted proof around in 1970. They were at two extremes: either fully inventive (e.g., using Robinson’s famous resolution principle) in searching for a proof, or fully noninventive in the sense that they would only check that each small step performed by a human was logically valid (as in de Bruijn’s Automath system). Both these approaches, by the way, contribute a lot to today’s proof technology.

I looked for something in between, where a human would design a tactic (or a strategy built from little tactics) and submit it to the machine together with the thing to be proved. There would be interaction; if one tactic failed or partly failed then the machine would say so, and the human could suggest another. The key thing was that, although the tactics could be adventurous, the machine would only claim success if a real proof was found. In ...