Go to the first, previous, next, last section, table of contents.


Edsger W. Dijkstra

I know of no biographical information whatever on Dijkstra, but he deserves mention for at least three reasons:

Dijkstra's theoretical contributions include the semaphores implemented internally or externally by virtually every modern operating system, and the three-color incremental garbage collection algorithm I (intend to) use in Muq.

Dijkstra is one of a number of brilliant early contributors to practical hardware and software engineering who subsequently became very dissatisfied with the perpetually bug-ridden state of the art, and turned to the study of ways of producing demonstrably correct computing systems.

(C.A.R Hoare, inventor of Quicksort, and David Gries, a compiler construction pioneer, are other examples. I would include Donald Knuth, except that he is a polymath who does everything from massive practical hacking (TeX) to pure mathematics to humor, making him harder to pigeonhole.)

To date, formal programming verification techniques have not had a great impact on mainstream programming practice, but few people can work for long in the field without becoming dissatisfied with the state of the art, and one cannot help but feel that at some point the current split between theory and practice of programming will close dramatically.

For a sip of vintage Dijkstra, I'd suggest: a discipline of programming, edsger w. dijkstra, Prentice-Hall 1976, ISBN 0-13-215871-X.

As an illustration of the current gap between the theoretical and practical wings of the computing community, I'd contrast Kernigan and Ritchie's assurance that all examples in their book have been tested directly from the text, with Dijstra's laconic comment in the above book that, "None of the programs in this monograph, needless to say, has been tested on a machine."

Dijkstra seems to me to have something of the shrillness of a brilliant pioneer feeling ignored and bypassed by the mainstream, but he is a profound analyst and synthesist who cares deeply about correctness, elegance and beauty in computing, and careful attention to him can hardly fail to deepen one's own understanding.

(Folks intrigued by the above book might look to Formal Development of Programs and Proofs, edited by Edsger W. Dijkstra, Addison-Wesley 1990, ISBN 0-201-17237-2 for a more recent survey.)

Why have formal programming techniques had such little little success as yet?

I'm confident that somefolk would reply more or less to the effect that most programmers are just too dumb and/or ignorant to apply them, but I think this cheap shot falls far short of the complete story.

First of all, few if any people would have the temerity to accuse Donald Knuth of being too dumb or ignorant to apply program proof techniques, but not even he chose to apply them formally to TeX when he wrote it.

To be sure, David Gries cites TeX as an example of a program written throughout with careful informal attention to correctness considerations, but Knuth offers a reward of $10.24 for bugs located in TeX, hardly suggesting absolute faith in the absolute correctness of the program.

Despite periodic media campaigns suggesting that formal program verification techniques are about to charge over the hill and rescue computing from the reliability crisis, actual application of the best techniques available have repeatedly had unsatisfying results. A Canadian project to use computer rather than mechanical controls in a nuclear reactor, led by Dave Parnas, one of the leading practitioners of the field, ended with the conclusion that if the project were redone, it would be better to stick with mechanical controls.

Further, even "provably correct" toy programs published in refereed journals regularly turn out to contain errors.

The fundamental problems appear to be:

  1. Program proofs are just as succeptable to errors as mathematical proofs, not to mention programs.
  2. Classical algorithms are short and tricky, but real programs are long and boring.
  3. It is frequently impractical to express the problem formally.

The first is a problem because whereas increasing our confidence in short mathematical proofs can reasonably be accomplished by publishing them and having the top specialists in the field debate them at length, this is scarcely an economic way to produce billions of lines of computer code annually.

The second is a problem because while the innovative algorithms that computer scientists devote their attention to tend to be short and tricky, both allowing and justifying application of proof techniques, most practical computer programs seem to consist of vast amounts of very straight-forward code which just don't reward proof techniques. The vast majority of coding errors are completely trivial when noticed. The real program reliability issues seem to relate more to dealing consistently with thousands of trivial constraints than a handful of difficult ones: One seems to need fiendishly precise bookkeeping more than brilliant insight.

The third is a problem because if you can't specify formally the requirements on the program, or if the specification is bigger and buggier than the program itself, formal verification is quite useless. David Parnas relates asking an engineer whether "the temperature exceeds 350 degrees" means exceeding it for a microsecond, or for some percentage of the time over some interval, or some weighted combination of time in excess times degrees in excess or just what... I think he got chased out of the office. But if even such an apparently straight-forward issue is problematical, imagine the difficulty of verifying that a program is "ergonomic" or whatever.

The real wins in reliability seem so far to have come from automating programming tasks, rather than analysing them: If the code produced is larger than the code producing it, then it can be analysed and debugged more thoroughly, and the resulting code quality may be much higher. An outstanding example is register allocation, which used to be done by hand by assembly programmers, clobbered registers being a perpetual source of bugs, and which is now done almost universally by compilers, clobbered registers being today an almost unknown problem.

That said, there does seem also to be an almost unnoticed, slow but steady spread of automatic program verification techniques: The typechecker in a compiler is in fact a specialized but useful theorem-prover establishing certain sorts of correctness properties on the program. There is steady progress in both the underlying dataflow analysis algorithms used to deduce program properties -- mostly with the immediate goal of optimizing the code -- and in the richness of the type language provided to the user: The type language of C is a huge advance over that of early Fortran, and the type languages of recent offerings such as Haskell are dramatically more sophisticated yet.

Will the next increments in program reliability come from just exhorting programmers to be more perfect? From more abstract languages which automate more of the code generation? From more effective typecheckers and type languages that understand more properties of the program? From programmers gradually learning to apply a deeper understanding of algorithmic structure to existing languages? From semantically more sophisticated code editors which produce programs known to be correct by construction? From switching to a different programming paradigm which makes programming simpler? From capitalizing on cheaper hardware by writing code which is less efficient but simpler and more reliable?


Go to the first, previous, next, last section, table of contents.