This chapter is from the book
This chapter is from the book
This chapter is from the book
Mathematics: 1968
The idea of software as a form of mathematics is a seductive one. There are, after all, many adjacencies. The early programs written by Hopper and her crew at Harvard were all numerical, and deeply mathematical in nature. The use of the Harvard Mark I to compute the solutions of systems of partial differential equations describing the implosion of the plutonium core of the Fat Man bomb required a very deep mathematical ability indeed.
It was, after all, Turing who claimed that programmers were “mathematicians of ability.” And it was Babbage who was driven by the need to ease the burden of the creation of mathematical tables.
So when Dijkstra wrote that software would become more and more a matter of mathematics, he was standing on pretty firm historical ground. He therefore focused his endeavors on mathematically proving software programs correct.
We can plainly see this in his Notes on Structured Programming,29 as he shows us the basic mathematical mechanisms for proving a simple algorithm correct. He outlines those mechanisms as enumeration, induction, and abstraction.
He uses enumeration to prove that two or more program statements in sequence achieve their desired goals while maintaining stated invariants. He uses induction to prove the same things about a loop. He uses abstraction as his primary motivation for black box structure.
And then, using all three of those mechanisms, he presents a proof of the following algorithm for computing the integer remainder of a/d:
)
This is a lovely little algorithm that runs in logarithmic time using a shift-and-subtract approach. Any PDP-8 programmer would be proud.
The proof that Dijkstra presented was two pages long, followed by another page of notes. My own proof, based upon Dijkstra’s, is a bit shorter but no less imposing (see next page).
It ought to be very clear that no programmer30 would accept this as part of a viable process for writing software. As Dijkstra himself said:
“The pomp and length of the above proof infuriate me […] I would not dare to suggest (at least at present!) that it is the programmer’s duty to supply such a proof whenever he writes a simple […] program. If so, he could never write a program of any size at all!”
)
But then he goes on to say that he felt the same kind of “fury” when examining the early theorems of Euclid’s plane geometry. And this is where Dijkstra’s dream shows up.
Dijkstra dreamed that, one day, there would be a body of theorems and corollaries and lemmas that programmers could draw from. That they would not be relegated to proving their code in such horrid detail, but rather would restrict themselves to techniques that were already proven, and could create new proofs based upon the old ones without all the “pomp and length.”
In short, he thought software was going to be like Euclid’s Elements, a mathematical superstructure of theorems, a vast hierarchy of proofs, and that programmers would have little to do other than assemble their own proofs from the resources in that vast hierarchy.
But here I sit, in the waning months of 2023, and I do not see that hierarchy. There is no superstructure of theorems. The Elements of software has not been written. Nor do I believe it ever will.
There is an odd parallel between Hilbert and Dijkstra in this regard. Both were seeking a grand edifice of truth that simply cannot exist.
Dijkstra’s dream has not been achieved. In all likelihood, it cannot be achieved. And the reason for that is that software is not a form of mathematics.
Mathematics is a positive discipline—we prove things correct using formal logic. Software, as it turns out, is a negative discipline—we prove things incorrect by observation. If that sounds familiar, it should. Software is a science.
In science, we cannot prove our theories correct; we can only observe them to be incorrect. We perform these observations with well-designed and well-controlled experiments. Likewise, in software, we almost never try to prove our programs correct. Instead, we detect their incorrectness by conducting observations in the form of well-designed tests.
Testing was something that Dijkstra complained about by saying: “Testing shows the presence, not the absence, of bugs.” And, of course, he was correct. What he missed, in my opinion, is that his statement proved that software is not mathematics, but rather a science.
