Submitted by egdaylight on
In his technical report (MR 34) of October 1961, Dijkstra explained why he viewed a good programming language to be one of a small number of very general concepts. To clarify, he used an analogy between mathematics and programming, an analogy which in later years would be scrutinized in several ways by his contemporaries. (See e.g. MacKenzie's 2004 book Mechanizing Proof: Computing, Risk, and Trust.)
In 1961, Dijkstra described a programming language "as a means of feeding programs into a machine" and openly wondered what it means for a programming language to promote "good use of a machine". He noted that leading German and British researchers viewed good use of a machine in terms of machine efficiency; he contrasted this with his own view that a programming language should primarily be a tool to achieve program correctness. Further details are presented in my paper `Dijkstra's Rallying Cry for Generalization ...'.
On the assumption that program correctness is vital, Dijkstra subsequently pondered about the criteria to be used in programming language design in order to avoid programming errors. The question to be answered was: Which criteria should be used in defining (and implementing) a programming language such that it helps the programmer write correct programs? To address this question, Dijkstra first elaborated on the notion of correctness, wondering what it means in the field of mathematics (as opposed to programming). In his words:
[I]t is impossible to prove a mathematical theorem completely, because when one thinks that one has done so, one still has the duty to prove that the first proof was flawless, and so on, ad infinitum. [...] One can never guarantee that a proof is correct, the best one can say is "I have not discovered any mistakes."
In response to the above concern, Dijkstra provided two reasons why mathematical theorems, nevertheless, do have a high degree of plausibility. Both reasons are sociological in nature and were (ironically) also used later by De Millo, Lipton, and Perlis in their now-famous 1972 paper `Social Processes and Proofs of Theorems and Programs' which scrutinized the very idea of program verification. Dijkstra's two reasons were:
- "[S]o many people have, each in their own way, derived these theorems, that there is a non-negligible probability that they do indeed follow from the axioms."
- "[T]he pretended conclusions are subject to conditions so orderly that the user's task of showing that he has applied the theorem correctly is not too cumbersome."
It is the second reason which is of concern here. It states that a theorem is useful only if it is applied under a minimum number of clear conditions. For example, a statement that distinguishes between prime numbers and composite numbers is useful, but a statement that distinguishes between 7 different cases is much less useful. Hence, the first statement, after being proved, is considered by many mathematicians to be a theorem while this is not (necessarily) the case for the second statement.
Now comes the analogy: Dijkstra noted that, just like the mathematician, "the programmer is in exactly the same position" for, he too, cannot prove the absolute correctness of his programs. The mathematician has theorems, the programmer has subroutines. If a theorem is only useful if it is applied under a minimum number of clear conditions, then — if the analogy is effective — a similar remark holds for a subroutine. In Dijkstra's words:
[T]he usefulness of a subroutine (or, in a language, a grammatical instruction) increases as the chance decreases, that it will be used incorrectly.
Hence there is a need for a small number of concepts in the programming language under design. These concepts, while few in number, are great in generality. This, in brief, captures Dijkstra's 1961 notion of elegance in his field of expertise, namely that of programming.
The question remains whether the analogy made by Dijkstra (and others) is warranted. Noting a similarity between the mathematician and a programmer does not exclude the possibility that there are one or more differences which make the analogy ineffective. Arguments of this kind have been presented repeatedly during the course of history. For example by De Millo et al., Fetzer, Dobson & Randell, Naur, van der Poel, Robinson et al., and Zemanek.