Chapter 9. ML
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 ...