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.
ahhh that feels so much better!
I don't care.
Is actually a language that is usable at this point, or just a spec?
was a paedophile faggot (its true, look it up)
Now that just makes feel so much more confident about his work...
The owls are not what they seem
I always wondered what "Officer Pete Malloy" from Emergency! was doing. I wonder if Randolph Mantooth and Kevin Tighe can pass the Turing test?
9 steps to greasing your anus for Yoda Doll Insertion!
v 3.76.0
$YodaBSD: src/release/doc/en_US.ISO8859-1/yodanotes/9steppro cess.sgml,v 3.76.0 2003/11/24 20:30:25 tsarkon Exp $
All in a days work with a Yoda figurine rammed up your ass.
I HAVE A GREASED UP YODA DOLL SHOVED UP MY ASS!
What you can do with you ass after sitti
rm@dcs.ed.ac.uk
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
I hope high gas prices are depriving your children, you fucking dumbass.
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?
Important Stuff:
Please try to keep posts on topic.
Try to reply to other people's comments instead of starting new threads.
Read other people's messages before posting your own to avoid simply duplicating what has already been said.
Use a clear subject that describes what your message is about.
Offtopic, Inflammatory, Inappropriate, Illegal, or Offensive comments might be moderated. (You can read everything, even moderated posts, by adjusting your threshold on the User Preferences Page)
If you want replies to your comments sent to you, consider logging in or creating an account.
Problems regarding accounts or comment posting should be sent to CowboyNeal.
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 is only a short drop from breaking one of God's laws to the other. Arguing semantics is pointless, the man was a sinner.
"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
He got away the last time. Make sure he hangs this time.
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.
Dear Dr. Milner:
As a fellow award-winning scientist, I would like to ask you: where do you see technology headed during the next 50 years? Do you feel that we will invest most of our efforts into improving our personal computing experiences, or are there more overarching goals for organizations operating collectively?
Thank you for your time.
Sincerely,
Seth Finklestein
I'm not Seth Finkelstein. I still speak the truth.
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.
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.
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.