Following the recommendation of a commenter to Proofs, Education and Open Problems, I ordered Dijkstra's "A Discipline of Programming" which arrived Saturday. I was able to sneak in a few minutes of reading while the baby was asleep and found it a delight. For your listening pleasure, I supply some selections.
On the language used in the book
...I came to the conclusion that none of the existing programming languages, nor a subset of them, would suit my purpose; on the other hand I knew myself so unready for the design of a new programming language that I had taken a vow not to do so for the next five years... I have tried to resolve this conflict by only designing a mini-language suitable for my purposes... --EWD, Preface, "A Discipline of Programming"I had to smile at the several points here, not the least of which was the conclusion that none of the current languages was suitable to the task at hand. A lesser man than I might be tempted to ask "why not use MIX?" (Knuth is listed in the acknowledgments). "Predicate transformers" are at the heart of the (mini-)language he did design.
On Dijkstra's life's work
After having devoted a considerable number of years of my scientific life to clarifying the programmer's task, with the aim of making it intellectually better manageable, I found this effort at clarification to my amazement (and annoyance) repeatedly rewarded by the accusation that "I had made programming difficult." --EWD, Preface, "A Discipline of Programming"After visualizing the expectations of parents, students, and employers from his depictions in "The Cruelty of Really Teaching Computer Science", this accusation could serve as a good summary, in the spirit of shooting the (particularly helpful) messenger: indeed, fully correct programming is difficult. (Or do I presume too much there? What do I know about fully correct programming?)
On manufacturing defects (revisited)
Finally, the book opens with an illustration that partly addresses my question about bugs appearing in an implementation of a provably correct algorithm.
In illustrating what is a computation by starting with something that is not, we are asked to imagine two pieces of cardboard: "The top one displays the text 'GCD(111,259)='; in order to let the mechanism produce the answer, we pick up the top one and place it to the left of the bottom one, on which we can now read the text '37.'" The major drawback Dijkstra points out is this:
No matter how carefully we inspect the construction of the mechanism, our confidence that it produces the correct answer can only be based on our faith in the manufacturer: he may have made an error, either in the design of his machine or in the production of our particular copy." --EWD, Chapter 0 "Executional Abstraction", "A Discipline of Programming"I feel this satisfactorily addresses my question about whether Dijkstra would call implementation bugs "manufacturing defects." Sort of nice to see that random question addressed in the first example of the first chapter1.
This drawback, that of faith in the manufacturer of mathematical results, is not a new one. Newberry Medal winner "Carry on Mr. Bowditch" accounts the life and times of 18th century sailor/navigator/mathematician Nathaniel Bowditch who bemoans the errors he finds in Moore's navigation charts. He fusses and fumes over these, saying "mathematics is nothing if not correct." Later has cause for grief when one of those errors causes a good friend to be lost to sea during a wreck2. When Dijkstra invokes "faith in the manufacturer" I can't help but recall these scenes, and the conviction in saving lives that drives Bowditch to publish his own navigational guide, checking and rechecking each figure. I see a future day when a combination of spectacular public software failures and a quality champion or twelve will bring us to a new level of software quality.
1 Not to be confused with chapter, being the second chapter counted.
2 What happens next? Read the book!