Social Processes and the Design of Programming Languages
In 1979, De Millo, Lipton, and Perlis wrote an article called Social Processes and Proofs of Theorems and Programs that ignited a firestorm in the software-engineering community. They pointed out that of the hundreds of thousands of mathematical theorems published every year, "[o]nly a tiny fraction come to be understood and believed by any sizable group of mathematicians."
One might think that it would be easy to convince mathematicians to accept a theorem by proving it. However, proof can contain errors, and there are claimed proofs even of mathematically important propositions that have gone for years before anyone discovered their fatal errors. Therefore, argued the paper, "a proof does not in itself significantly raise our confidence in the probable truth of the theorem it purports to prove."
If a proof does not convince mathematicians that a proposition is true, what does convince them? The paper argued that mathematicians come to believe in the validity of a theorem through a social process. Not only do they check the steps in a proof, but they internalize the knowledge behind the proof, connect that knowledge to what they already know, and see that this new knowledge fits in useful ways with what they already know. The existence of an apparently correct proof is far from sufficient by itself to convince mathematicians of its validity.
The authors went on to argue that the same phenomenon should apply to proofs of programs, but "because no comparable social process can take place among program verifiers, program verification is bound to fail." They used this line of reasoning to argue against the general notion of proving in a mechanical way that a program follows its specifications. As a hypothetical example, they described a programmer running a 300-line program through an automatic verifier and receiving a 20,000-line proof of the program's validity. Because of the complete absence of a social process corresponding to the one in the mathematical community, there is no reason to believe that even such a proof would convince the programmer of the program's correctness.
This article provoked a blisteringly angry response from Edsger Dijkstra called On a Political Pamphlet from the Middle Ages. He justified his title by making the claim, among others, that "the paper is pre-scientific in the sense that even the shallowest analogy is accepted as justification." Obviously full of anger, he likewise accused the original authors of similar anger, saying that the paper "leaves the reader wondering why they [the authors] have put so much venom in their text, because they seem to have gone much farther than the usual practitioner's backlash."
These two articles set out two sharply contrasting views of mathematics, which we might call pragmatic and formal, respectively. The pragmatic view is that mathematics is something that people do, so its intellectual sway will ultimately depend on how it affects the people who practice it. The formal view is that a correct proof starting from valid premises will yield a correct result, and people's opinions should hold no sway.
Thirty-five years later, it seems to me that these articles symbolize a conflict that still pervades the software community — especially as far as programming-language design is concerned — without many of its members even being aware of it. For example, I have lost count of how often I have heard arguments such as "How can anyone still be using a language that doesn't do runtime validity checking on every operation? Don't you know that such a language is nothing more than a security nightmare waiting to happen?"
At first, such an argument is hard to answer. After all, there is no question that failure to check operations' validity at runtime is indeed a rich source of opportunity for malware. In that sense, the formal argument is unassailable.
However, there are several pragmatic arguments on the other side; taken together, they are probably at least as strong as the formal argument, and perhaps even stronger:
- It is not enough to define a semantically safe language; one must also convince programmers to use it. In the early days of C++, many attempts at making the language semantically safer were countered by prospective users saying, "If you break this feature of C, we won't be able to use it." And C++ would have had no chance at all of widespread adoption had it not been attractive to a substantial number of C programmers.
- Semantic safety through runtime checking often comes at the cost of performance. Sometimes programmers can afford that performance overhead; other times, they can't. Perhaps most often, they don't know whether or not they can afford the overhead, so they avoid it just in case.
- Although it is tempting to believe that runtime checking will prevent security problems, last week we saw an example of how bugs in that runtime checking can yield security loopholes that are even nastier, because they are present even without any bugs in user code. Adding automatic runtime checking increases the amount of code that must be right in order to avoid security problems, and by doing so, can make those problems even harder to avoid.
In other words, what we have here is a formal argument in favor of formal solutions to programming-language design problems, and a pragmatic argument in favor of pragmatic solutions. I think that this tension between formal and pragmatic design approaches is every bit as capable of generating acrimonious conflict as it was in 1979.
In the coming weeks, I'm going to talk about some examples of this conflict and try to explain the arguments on both sides.