Interview With Turing-Award Winner Robin Milner

Martin Berger writes "Turing Award (1991) winner Robin Milner is one of the most influential computer scientists. He may not be as well-known as he deserves to be, but his research contributions are ubiquitous: he developed the first mathematically sound yet practical tool for machine assisted proof construction. This research has been continued successfully and led to many useful proof assistants such as HOL, Coq or Isabelle that are being used heavily for verification purposes today." Read on for more information about Milner, and a link to Berger's excellent interview with him. Berger continues "There is also a direct line from this strand of Milner's work to what may be one of the hottest topics in computer science: proof carrying code. Milner also headed the effort to develop ML (best known today by its descendant Ocaml), the first language to include polymorphic type inference together with type-safe exception-handling and module mechanisms. Most modern programming languages can trace some of their advanced features directly back to ML's pioneering efforts. Most of all, he established concurrency theory as a scientific field by creating and studying idealised concurrent programming languages like the Pi-Calculus. That calculus is becoming more and more influential in the design of new programming languages (for example Microsoft's XLANG) and the WWW infrastructure. A few weeks ago, I interviewed Milner. I wanted to find out about the man and the stories behind all this great research. I hope you find it as interesting as I do. The transcript of the interview can be found here."

Comments

Formal proofs?

[heironymouscoward]

One of the first things I learned as a computer scientist was the impossibility of proving a piece of software "correct".

Still, I always found it an interesting concept.

Then, one day, watched a Eureka (EU) team build a formal verification suite based on Z. One of my friends was on the team. One of the best programmers I ever knew, he decided the whole venture was a fraud, said so, and was fired.

My opinion? Formal proofs are a holy grail, unreachable, and the reality of software is that small, testable, interworking pieces is the only way to assure "correctness". That, and code generation, the wizard's wand of software.