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."
First we should make the distinction between Integral Calculus and other calculi such as the pi-calculi and the lambda-calculi. The Integral Calculus can be categorized as continous math, while the pi and lambda calculi can be put under the label of "discrete math" as both pi and lambda calculi are term rewrite systems.
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.
One thing that you have to understand is that there are still people out there that think that "math" means numbers, and therefore sophisticated numerical math such as the Integral Calculus is crammed down everyone's throats. I think that for most people, a more conceptual math based on category theory or set theory or somesuch would be far more useful in the long run.
Er, what?
One thing you should have learned as a computer scientist is the proving a peice of software correct is *possible*.
The caveat is that you can only prove it correct with respect to a formal specification (as we all know if your spec is wrong your still shafted) and formal proofs are hard to construst for non-trivial programs. Hence the need for machine assisted proof tools.
as both pi and lambda calculi are term rewrite systems.
...
i'm not sure calculi like lambda or pi can easily be classified as term rewrite systems because of (1) alpha conversion, i.e. renaming of bound variables; and (2) because of all the coinductive stuff that you have in the definition of the congruence relations that you use to quotient the syntax with
Because Differential/Integral Calculus makes up the basis of, well, everything. Understanding D&I Calculus has allowed me to grasp both concepts that I could sort of understand, but never really comprehend, and new ideas that have expanded my awareness of the world around me.
For starters, lines, curves, and surfaces, the very basics of geometrical mathematics, has differentials and integrals as a fundamental idea that surrounds it completely. As a person who enjoys doing 3D modeling and is currently hired as a writter of 3D tutorials, Calculus has enabled me to have such a deep understanding of the material that I am able to explain it to others with ease, including those who have not had calculus or even trig classes!
Second off, Calculus relates to Physics. Anyone can be taught to memorize Physics equations, but once you know calculus, you can derive them yourself! It is a far better feeling to have a good solid theoretical understanding of the material being covered rather than just saying "well this equation fits to the data decently well so it must be true."
The first, is a scientific mind set. The second is what a business major learns.
Continuing on the physics note, Calculus is used in an understanding of how the basic fundamentals of computers work. Being able to say "take the derivative of it here" and have it make sense, ah, a lovely thing. Hell, anytime you have units and notation being thrown around, Calculus can make itself handy. A lot of relationships in the natural world only show up if you understand what taking the differential or the integral of something does to its units.
Then there is Linear Algebra, which is VERY fundamental to computers. Matrixes are used throughout computers of all types and sizes, (with some limited exceptions, yes yes ), teaching Linear Algebra becomes far easier if the students are required to learn Calculus first. Heck everything becomes easier after Calculus is learned.
You are also ignoring that, at its heart, all mathematics are related. The more a person understands in any field of mathematics, the more they can learn in all other fields. Calculus forms an excellent base for more knowledge to be built upon, and even if sight of that base is (unfortunately) lost by the student over time, it still exists there as a foundation for all that the student has learned.
(That, and, quite frankly I found Calculus to be fun.
Need help treating your acne? Come here!
Almost no branch of computer science has seen more countless hours of research devoted to it with more meager results then program verification theory. (And that is not primarily what Milner's work addresses.) The fundament problem with program verification, and why you will not see any of the applications the you mentioned for at least the foreseeable future and probably ever, is that even after you've developed a language that is amenable to correctness analysis and after you have developed a specification requirements language to articulate the 'implication' of your programs written in the verifiable language, and after you have built a tool that allows you automate the construction of correctness proofs, you find that all you've done is push the real problem solving work of programming (where most of the errors come from) into a fuzzy realm of prerequirements that is even less conducive to the types of problem solving that programmers do then the original programming language. 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.
Ignorance abounds. Just because it is hard to verify some properties, we should ignore verifying those that we can?
I'm a CS and Math guy... to preface this opinion
Now it depends on the program and the school of thought. Anyone who's ever worked with a physicist in the tech business (they crop up from time to time) understands that the guys with the PhD in Phyiscs is almost always better than the guys with Masters in CS, it just works out that way. Physics and Calc are one in the same when you get through all the BS.
Everyone knows that physicists are better and so there is a desire to teach the tools that they use. That's just a theory I have, nothing to back it up other than everyone knows how Einstein was and everybody has an idea who Hawking is and nobody knows who Turing was or Euler was or Galois. If it wasn't for Russle Crowe a fair number of math geeks wouldn't know who Nash is... Copy what works.
Secondly, better programs tie it all together. You can start off simulataneously learning continuous calc and Zermelo set theory in a discrete class. Keep learning calc and more discrete. Then throw some linear algebra in and some abstract algebra and then right about that time one of them (the way I had it, it was a calc class) goes into the throes of a mathgasm and proves Euler's formula, using discrete math and calc both and kind of ties the whole thing together (because after you've learned all the different methods of integrations you're spending a lot of time doing what a class mate of mine called "that big E shit" with additive and multiplicitive series...) If all goes well you'll be wondering what's the true "key to math" at about this time and it's kind of like having God whisper in to your ear when you see how it all links up. I think proving a lot of the linear algebra stuff is substantially easier if you have calc as a tool. Then you continue on and prove all of the calc stuff using the set theory that you had been building up, take a few more calc courses doing diffeqs, partials and calc in 3d which is all mostly mechanical at that point and then after all of that you do whatever the hell you want in math. I think most of the stuff in typical stats classes is very difficult to prove without calc.
The link between linear algebra, abstract algebra and discrete math is pretty easy to see as you're doing it. The bridge between discrete and continuous math is a bit more complex but it's really undeniable when you see it.
I expect this is true, but if I may...
"all you've done is push the real problem solving work of programming (where most of the errors come from) into a fuzzy realm of prerequirements that is even less conducive to the types of problem solving that programmers do then the original programming language."
By prerequirements do you mean identifying the behaviors and properties needed at each level of programming? I know this won't suddenly enable the creation of "perfect" programs but if errors are occuring in the design of the software rather than the code implimentation, hopefully they would be easier to address by identifying that behavior and tracking it back to the specification. Specifying how a program will behave is something I know we aren't terribly good at, but if we want really secure and reliable software its a hurdle that must be overcome.
"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."
I guess it depends on what you mean by general purpose - I guess I don't really think of something like a database or spreadsheet as general purpose. They accept specific types of input, and perform specific operations on input, and return well defined output. If you define these types and the behavior for the types, and clean failure for other input types, shouldn't that be enough to specify the behavior of the program? Obviously there are a lot of specific points, such as allowable cell input, sheet formatting, operation specific input, etc. but I guess I don't see why it couldn't be attacked. Undoubted this is simply my ignorance. Are there any good introductory references to this kind of thing?
"I object to doing things that computers can do." -- Olin Shivers, lispers.org