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

remember MegaHAL

[DarklordSatin]

Mention of the Turing Award brings back memories of all the fun times we had with MegaHAL (http://megahal.sourceforge.net/). We set up a machine in my local dorm kitchen and our MegaHAL rapidly became a horrible swearing bigot; it provided endless amusement for all.

Proof of Code

[starseeker]

I have been wondering for some time now if proving code might be the next step in computers. If you think about it, most problems related to everyday use of computers have been solved, in one form or another - spreadsheets, word processors, databases, and communications seem to account for most of what we want to do, and their feature sets are largely well defined. The task now is not to figure out what we want to do - we know that very well. What we want to do now is do it WELL.

I know little about the field of proving code, so whether this is possible I don't know, but it would be interesting to try something like the following:

a) create a large, detailed specification of what a database (for example) should be able to do. Start general and work down to specifics. Map the full feature set out, eventually down to the function level.

b) translate those requirements into some proof language - Z or B are one's I've heard of, perhaps there are others more appropriate. Identify what the limits are - ultimately the behavior of the program should be well defined, ideally. Break it down to a point where the individual units under consideration can be reasonably expected to be provided by the operating system or system libraries (which, in an ideal world, would also have been created or could be created by a similar process).

c) Having the proven structure, use code generation techniques to automatically produce code that will create the program.

In essense, basically all the work would be done at the specification level, and once we can specify in full detail what we want, the computer itself handles the job of writing the actual code.

As I said, I don't know how much of this is possible, but if we were to start from scratch at the assembly level perhaps something like this could occur:

0) Before anything else, based on language specs, create a proven compiler for the language(s) to be used. Without that, all practical work is useless.

1) Define kernel or microkernel design, and map that design down to hardware levels (RISC might be an easier platform for this). EROS might be a good design starting point. Once it is clear what jobs the hardware would need to do for each command, map out and prove the assembly commands in the RISC platform that would do each job. Build off of those proven components to prove the behavior of each higher level language command, and once the higher levele language behavior is defined and matched to what is needed, write and prove the kernel.

2) Having a kernel whose behavior is now well defined and trusted, the real work begins. Working off of the well defined and proven components in the kernel, build up the rest of the tools needed to provide an operating environment expected on a modern machine. Compartmentalization is key, both for system security concerns and for proof concerns. Essentially the unix idea of one tool doing its specific job correctly, taken to its logical extreme.

3) Having a basic system developed, begin to work on the end user components. Graphics libraries and toolkits would need to be implimented and proven. Porting current toolkits would be possible, but the would likely not be suitable for the rigorous hard core proof testing and a major system graphics setup would have to be designed, specified, and created. Fresco might be a good source of ideas here. Once the proven structure is available,

4) Identify and specify key end user applications. Define an Office application, with various components like word processor and spreadsheet, and define clearly their features. Treat the last 20 years of software usage as field research on what features are required. Impliment them using the proven system tools. As they mature, replace ports of non-proof based tools with new software. Instead of having many tools for one job, define the job itself clearly, and its solution clearly. If more features are needed or desired, the place to add them is in the proof structu

Re:Proof of Code

[Anonymous Coward]

These techniques can be useful for very narrow, specialized types of applications which must be correct. But can never work for something even as specialized as an operating system, let alone a general-purpose business application.

This is correct, BUT the applications for which you really NEED verified correctness are so vital (for example airplane software) that we cannot afford not developing the formal methods. That research will spin off to more general purpose software. Just look at the countless millions, if not billions companies like Intel or Microsoft throw at formal methods now (for example in the form or model checking, eg SLAM).
They do this, because they have taken huge economic hits from faulty software/hardware ...

The first 2 decades of formal methods were abysmal in their results, but this is changing now. Model checking for example really is a succesfully technology.

Re:So he's the one

[CharlesEGrant]

I am still trying to figure out why Integral Calculus is forced down everyone's throat. Computer Scientists are better off studying proof theory, axiomatic set theory, lambda-calculi, etc...

There are subfields within CS that make use of Integral Calculus... but most subfields of CS do not use it and instead use things like proof theory, set theory, etc

Most undergraduates do not have an accurate idea which field, let alone which subfield, they are going to end up in. The integral/differential calculus is a gateway topic. If you don't have it you've foreclosed study in many areas: physical sciences, numerical methods, probability and statistics, much of engineering, economics etc. I agree that the lambda calculus belongs in every CSci undergrad education, but lacking proof theory or axiomatic set theory closes very few doors, interesting topics though they may be.

In practice, the average CSci B.S. is going to end up writing database front ends for a business somewhere, so you could argue that all of these topics are academic and irrelevant. I just think that the first two years of college are too soon to drop out from so many areas of human knowledge.

I worked with Robin Milner...

[C A S S I E L]

...way back in the mid to late 80's, mostly doing compiler programming in the ML project. In fact, my first exposure to ML was in 1979, with an early version running on on DECsystem 20. (I can't remember what it was written in - something like Lisp or Prolog.) For my Ph.D. I implemented a polymorphically typed hybrid functional/logic language based on the ideas of Milner and Ehud Shapiro.

The big push to ML as a language was, as stated, a redesign and implementation (in Pascal, I think) on VAX/VMS by Luca Cardelli back around 1981 - it was a lovely piece of design, with first-class records and union types, and pattern matching. During the standardisation of the formal semantics (late 1980's), the implementation effort was shared with Dave MacQueen at AT&T and Andrew Appel at Princeton (whose compiler books and papers on continuation passing are a good read).

Throughout, the implementations and the mathematics advanced hand-in-hand; on many occasions I'd be doing something in the compiler, and referring to the formal equations of the static or dynamic semantics to make sure I was doing the right thing.

I've been out of touch for about ten years (just when the Pi-Calculus was emerging) but my patterns of thought and reasoning about software structure are still rooted in the experiences of a quarter of a century ago, and I still come across things whose lineage can be traced back to ML's theory and practice (for example, Java exceptions and inner classes).