O'Reilly logo

Masterminds of Programming by Chromatic, Federico Biancuzzi

Stay ahead with the world's most comprehensive technology and business learning platform.

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, tutorials, and more.

Start Free Trial

No credit card required

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 ...

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, interactive tutorials, and more.

Start Free Trial

No credit card required