Slashdot Mirror
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."
So he's the reason I have to take so much calculus to be a computer programmer.
Is actually a language that is usable at this point, or just a spec?
Now that just makes feel so much more confident about his work...
The owls are not what they seem
How do we know that the interview is with the Turing Award winner? Maybe the interview was just with a computer?
GF.
Obligatory disclaimer for the Comic Book Guys out there:
I know, I know -- the Turing Prize isn't the Loebner Prize. It's the day before a holiday -- give it a rest and laugh a little.
Lots of petrified grits
Coq and Isabelle are used heavily "for verification purposes" today. ... poor old Isabelle... Give a girl a break!
Simon.
Physicists get Hadrons!
Wasn't that the lame 1970s show with Nurse Nipples or whatever her name was on it?
so even with the help of a computer your dumb ass is whining about learning math that newton and Leibniz discovered in the late 1600's.
get with the times. (there is evidence that archimedes understood infinity much more than realized before with new evidence, and he lived in 225 BC. )
care to whine about calculus anymore?
Must have been warm there.
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.
Ceci n'est pas une signature
"It doesn't rain because it is so dry" as Milner said in the interview in regard to the Suez Canal region.
But such banalities aside, it is an interesting interview. I was particularly interested in learning that he doesn't have a doctorate -- on this side on the pond that would have been required (for better or worse) for his academic position.
I can't believe this news is real. Its perfect timing though because I just finished up a report, I am studying this. This amazes me because I could not find any person on earth who has passed the Turing Award, by designing an OS that could trick people into thinking it was a person, and not computer hardware. In actuality (if we believe this news) it happened over 12 years ago and nobody has done it since. Sounds like this guy knows his stuff. Anybody else pass the Turing Award since? Anyone?
click here to incinerate homeless people
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.
The Turing Award has nothing to do with the Turing Test. It's just an award given by a major computer science association (the ACM) to people that they consider to have significantly advanced the field.
http://www.acm.org/awards/taward.html
This can't be /.'s own Robin Miller (roblimo), can it? Of course not, it's Robin MilNer!
-3Suns
~~~~
The Revolution will be Slashdotted
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
"I object to doing things that computers can do." -- Olin Shivers, lispers.org
Man, you pass the 'Turing Test'... you don't 'pass' the award.
I don't think just because you win the Turing award you win the test.
I agree wholeheartedly. Take care, see you next week.
Dad
( Comment source.)
The Independent: Reverend Spooner Arrested in Friar Tuck Incident - ISIHAC, Historical Headlines
Of course it's going off the rails. How else is it ever going to fly?
When microsoft first submitted XLang to OASIS, their primary criticism is XLang was poorly thought out. I don't know the validity of XLang being inspired by pi-calculus, but it definitely comes no where near it. If anything, XLang is simply glorified if/then statements in XML format. You're better off with other markup languages like RuleML that actually tries to learn from pi-calculus, horn logic and first order logic to create a well formed language.
Q: How do we determine who gets the Turing award?
A: By finding a geek who can pass the Turing test.
Yah, he killed himself because of persecution by the British authorities. Wonder why it's considered bad to point it out.. I'd always hoped that homosexuals would mention people like Turing more often than just the same old run of the mill "creative, artistic writer, singer, actor types" If I was gay, I'd be annoyed by the prevailing homo-stereotypes.. eg 'Queer Eye for the Straight Guy' (variations on flaming queen to touchy feely style maven) or well.. nevermind.. I just find it odd that you never hear it mentioned that Turing or Hardy (well, they could claim him.. since he seemingly wasn't heterosexual) or any number of scientist who weren't openly gay.. (but "might" have been.. oh well, we shall never know)
p
Or how's about John Maynard Keynes, the economist? Anthony Burgess' _Earthly Powers_ has a very funny running joke about how many of the greatest and most serious thinkers of the twentieth century were gay (or non-straight, in any one of a number of ways).
An excellent biography of Turing that explicitly deals with the significance of his sexual outlaw status is Andrew Hodges' Alan Turing: The Enigma. Makes one think of the expression "the backroom boys" in an altogether different way.
I don't think that Turing wanted to be a "sexual outlaw", by the way - obviously he'd have preferred it if the authorities had simply left him alone - but there is a subversive, anti-authoritarian streak in him which has some of its roots in the British gay culture of his times. An often overlooked aspect of the Turing Test is the stipulation that the human participants must also pretend to be something they're not - namely a member of the opposite sex...
Experience is a hard school, but fools will learn no other.
Hey-o!
One of the first things I learned as a computer scientist was the impossibility of proving a piece of software "correct".
You learned wrong. While it is known to be impossible in general to prove (or disprove) arbitrary properties about arbitrary pieces of software, there are still lots of specific things you can prove about specific pieces of software. The same is true for mathematics: we know that not everything can be proven or disproven, but that doesn't mean mathematicians stopped doing proofs.
In any case, you also misunderstood what Milner was working on.
spit
The late Floyd, of Stanford, had two B.S. but no advanced degrees. He was perhaps the inventor of nondeterminism, program verification (see "On the meaning of programs"), and of the Floyd-Fulkerson algorithm.
Verification, or at least the proof of correctness of optimizations is certainly not a meager result. However, there is an incredible amount of research that goes into this without huge results, just very respectable.
I agree, generally, that what falls under 'discrete math' (see, for example, "Concrete Mathematics" by Knuth et al.), is more important to the CS guy than, say, differential equations.
However, as a point of interest, I do know that Integral Calculus is not restricted to sets that are isomorphic to the reals, and hence is applicable in the discrete sense, as can be found in discussion of measure and integral theory. This is useful especially in generalizing series and distributions. Series and distributions are clearly very important in CS topics like complexity, counting, probability, etc.
You think that's bad? I've got a friend who's working on feeding Isabelle to the Vampyre.
guess you're ready for your yoda doll now.
Few humans could pass the turing test in the way turing outlined it - Have a human start the test, and then switch over the computer at some point later on without telling the questionee.
-
Lamda calculi is different from your usual calculus that involves integration and differentiation - it's more symbolic processing and discrete maths, and can be traced back to even church/turing, so you can't really blame him for it.
now some anecdote:
I took an undergraduate communicating automata/pi calculus course in cambridge in 1996 - I also had the good luck to be supervised by prof Milner himself (who was the head of the Computer Laboratory at that time) for that course. Then, you could download his notes as
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).
Did you get a temporary or permanent position in Edinburgh?
I got a permanent position in 1973. That was coming back from the States, which was a good thing because we wanted our family to be educated in Europe, not in America.
What do you make of the increasing patenting ideas in computing?
It's terrifying. It's ridiculous and terrifying at the same time.