Arthur John Robin Gorell ("Robin") Milner

Peter Landin’s ISWIM (“If you See What I Mean”) is an imperative programming language with a functional core, which means that it can directly implement many mathematical functions as computational values. Furthermore, it supports the definition of inductively defined datatypes. These allow us to implement directly the inductively defined abstract syntax of a formal language, such as Dana Scott’s LCF. Milner’s ML adopted these core features.

ML also supports the definition of abstract datatypes, whose elements may only be constructed by specified functions. Mathematically, the set of theorems of a formal system, consisting of a set of axioms and fixed rules of deduction, is inductively defined.  Each axiom is a theorem, as is the conclusion of any rule whose premises are axioms. ML’s abstract datatypes provide a computational framework within which this mathematical definition can be directly implemented. Every object of the abstract type Theorem must either be an axiom, or derived from other theorems by application of one of the rules of deduction. This guarantees that every Theorem has a proof.

Many complex formal systems can be naturally encoded in the computational metalanguage ML. Further ingredients were required to make it a practical tool. For example, a practical programming language should make efficient use of the programmer’s time, and should compile to efficient code. To relieve the programmer of the burden of annotating every value with its type, Milner independently rediscovered, implemented and extended Roger Hindley’s earlier work on type inference. In ML, types are automatically inferred by the system at compile time. So a program that compiles successfully cannot encounter type errors at run time. Polymorphic functions can be reused with different types.

Proof tactics encoded in ML can fail. For example, we can try proving something by induction on n, and fail because we don’t have a strong enough induction hypothesis, simply because our goal has the wrong syntactic form. ML allows a computation to fail by raising an exception that can then be handled by execution of an alternative computation. This allows us to combine tactics by trying one, and if that fails trying another. We can also apply a tactic repeatedly, until it no longer applies, or apply a list of tactics sequentially.

Rules, proof-states, tactics, and the tacticals, that build new tactics from old, are all encoded using higher-order functions. Rules are functions from lists of theorems (assumptions) to theorems (conclusion); proof states also include functions from lists of theorems (proven subgoals) to theorems (proven goal); tactics are functions from proof-states to proof-states; and tacticals are functions from for creating new tactics from old.

ML also includes facilities for imperative programming using mutable values, which allow the ML programmer to implement algorithms for making in-place updates. Exceptions and mutable values require subtle adjustments to the type system, and new semantics. ML provided a concrete bridge between theory and practice, and inspired new research in both type systems and semantics.

Oral interviews

Robin Milner was interviewed by Karen Frenkel and the transcript published in the January 1993, Vol.36, No. 1 of the Communications of the ACM. That interview is available here.

The transcript of an interview with Robin Milner conducted by Martin Berger in Cambridge on 3 September 2003 is available here.