What this talk essentially proposes is to scrap the teaching of an approach to program development that has produced pretty much EVERY SINGLE piece of practical software used in the history of computing, in favor of an approach that had not produced, to my knowledge, a single nontrivial piece of software by 1988, when the talk was given, and has not produced, to my knowledge, a single piece of software in the 20+ years since.
In a separate thread, I have posted De Millo, Lipton, and Perlis' 1979 argument against formal methods: http://fresh.homeunix.net/~luke/misc/p271-de_millo.pdf and 30+ years after that article, and 20+ years after Dijkstra's talk, I don't see how there can be an argument as to which of the two views has prevailed in practice.
I would welcome hearing Dijkstra's view argued, but I would find such an argument much more compelling if it included citations of actual, working programs (as opposed to isolated algorithms) that were developed with end-to-end formal methods. It would be even more compelling if the argument included published proofs of such programs and/or the author's personal experience developing them.
Had this done to me, in 1981 or so at the University of MD. They decided to teach some kind of "theory of proving programs correct" to a bunch of CS-101 types who were just learning Pascal, too. I guess the hope was that we'd get a healthy dose of mathematical proofiness and write better programs.
One of our first lectures: "Taking this loop, we prove by induction that it computes the sum of the first ten integers. Here are a bunch of logic formulas (lots of scribbles on the overhead). Here's a bunch of notation, it's got CONJUNCTION and DISJUNCTION and COMPOSITION and so forth. By inference [and some hand-waving] this five line program computes a sum, yes?"
Class: "Huh?" Not even panic, just a collective, bug-eyed "<I>What the fuck?</I>?"
The approach failed miserably; what it /did/ successfully teach was cynicism; most of the students were really upset at the obvious nonsense. [I was the only one of about 250 students to complete all the project work . . . and I cheated by writing the project in LISP, and writing a LISP interpreter in Pascal]
People certainly have written real software using formal methods: http://compcert.inria.fr/ is a good example.
Of course this does not constitute an argument that programming must be taught as a formal discipline, but it does indicate that formal methods can be useful in some circumstances.
Interestingly, http://compcert.inria.fr/release/Changelog mentions various "bug fixes" in almost every release, and the mentions of "successful tests" are not quite canonical either, but it certainly looks like a successful, nontrivial program.
Yes, CompCert is no timeless perfect gem. You could make a convincing argument that it's not really verified software in the Djikstra mold at all (only parts of the compiler are verified, although they are fairly large and interesting parts).
It does make a nice poster child for formal methods though.
I mostly agree with him that the paper is poorly argued (I have no love for formal verification). However he ignores the most salient point that it makes: that the effort of verification must be applied everytime a programmer makes a change to a codebase.
Entirely appropriate, assuming the post is interesting, which this one is. Pity it got lost in the shuffle.
Advocates of formal verification of software remind me of the old joke, usually about a Frenchman but sometimes about an Irishman, who says in some policy debate: "I can see that it works in practice, but will it work in theory?"
In a separate thread, I have posted De Millo, Lipton, and Perlis' 1979 argument against formal methods: http://fresh.homeunix.net/~luke/misc/p271-de_millo.pdf and 30+ years after that article, and 20+ years after Dijkstra's talk, I don't see how there can be an argument as to which of the two views has prevailed in practice.
I would welcome hearing Dijkstra's view argued, but I would find such an argument much more compelling if it included citations of actual, working programs (as opposed to isolated algorithms) that were developed with end-to-end formal methods. It would be even more compelling if the argument included published proofs of such programs and/or the author's personal experience developing them.