A Bridge too Far: E.W. Dijkstra and Logic

1. Introduction

Shortly after the death of E.W. Dijkstra (1930-2002), K.R. Apt wrote an obituary under the title Portrait of a Genius [1]. At the time it seemed to me a bit over the top. Now, with the added wisdom of the intervening years, I consider the title accurate. The most striking feature of EWD’s career was that his remarkable string of successes was followed by a debacle: the book on logic that he co-authored. In this article I list EWD’s achievements, sketch their significance, and try to penetrate into the reasons why he attached such value to logic.

2. Highlights

Let us consider the highlights in EWD’s work.

• Shortest path algorithm (1956)
  Started the industry of graph algorithms. For the genesis of the algorithm see [1a].
• Compiler for Algol 60
  Algol 60 has been characterized by C.A.R. Hoare as [2]

  … a language so far ahead of its time, that it was not only an improvement on its predecessors, but also on nearly all its successors.

The committee in charge of the language’s definition was divided on whether the language could be implemented even when its report was approved in January 1960. By the summer of 1960 the Algol 60 compiler was completed by EWD and J. Zonneveld.

• Concurrent programming
  In the late 1950’s EWD had the task of designing the I/O routines for the Electrologica X-1, an early computer with interrupts. This set him thinking about a suitable abstraction to deal with the new phenomenon of non-reproducible behaviour of hardware. By 1961 he had invented the semaphore, which featured in his 1965 paper “Cooperating Sequential Processes” together with the introduction of the mutual exclusion problem and critical sections. This started a flurry of activity in search of ever better synchronization primitives of which the monitors of Hoare and Brinch-Hansen are an example.
• The THE operating system
  At the first Symposium on Operating Systems Principles (1967) EWD reported on the structure of the multiprogramming operating system for the Electrologica X-8 developed under his leadership at the Technical University in Eindhoven. The audience was impressed, hearing for the first time concepts that have since then been widely adopted. One in the audience, surprised at getting answers to detailed questions, said: “You mean, did you people implement all this?”
• Structured programming
  As far as I can tell EWD invented the term “structured programming”. The earliest occurrence I found was in EWD249 under the title “Notes on Structured Programming” dated August 1969. The term escaped into the world at large with the Academic Press (1971) book authored by O.J. Dahl, E.W. Dijkstra, and C.A.R. Hoare with title “Structured Programming”. The book consists of three parts, each attributed to a single one of the three book authors. I presume that the book title was taken from Dijkstra’s contribution, which is EWD249, possibly revised.

“Structured programming”, the term, took off like a rocket. The extent to which it set the academic programming world abuzz is illustrated by the fact that there are in Knuth’s 1974 “Structured programming with goto statements” [3] about 35 references where I can tell from the title that they are about structured programming.

The publication of the book had the effect of turning the largely negative reaction to “goto statement considered harmful” into a positive one. It was as if the world said: “Now I see what you mean.”

• Non-determinism
  In 1967 R.W. Floyd had introduced non-determinism as an additional language feature. The proposal concentrated on how to implement it. For EWD it was a subtraction: by avoiding what he considered overspecification, it became a natural consequence of the semantics of the guarded-command language [4a].
• Self-stabilization
  So far EWD’s contributions were instant hits. Self-stabilization, on the contrary, was truly a sleeper. The concept was introduced by EWD in 1974 in a two-page paper [3a]. It was ignored until 1983, when its importance was stressed in an invited talk by Lamport. Apt and Shoja [3b] sketch its meteoric rise since then. They count 2000 references and report the 18th annual Self-Stabilizing Systems Workshop by 2016.
• Vivid examples and terminology
  EWD has been successful in coining terminology that sticks in the mind:
  • banker’s algorithm
  • critical section
  • deadly embrace
  • dining philosophers
  • guards
  • semaphores
  • sleeping barber

  3. “A Discipline of Programming”

  In 1976 EWD published a book under the title “A Discipline of Programming” [4], here referred to as DoP. It has two components.

  3.1. Neat algorithms

  From the preface I quote

  … on the one hand I knew that programs could have a compelling and deep logical beauty, on the other hand I was forced to admit that most programs are presented in a way fit for mechanical execution but, even if of any beauty at all, totally unfit for human appreciation.

  EWD had in mind a collection of neat algorithms for which even Algol 60 was not good enough to do justice to their “compelling and deep logical beauty”.

  3.2. Guarded commands

  In “Guarded Commands, Nondeterminacy and Formal Derivation of Programs” [4a], EWD presented the guarded-command language as one in which it is possible to formally derive programs from their specification in the form of a postcondition. The derivation then yields both the program and the preconditions giving the initial states from which the final states are guaranteed to satisfy the given postcondition. In addition to this remarkable innovation, the guarded command language has the property that its use brings out in the open the logical beauty of certain algorithms, otherwise unfit for human appreciation.

  4. Remarks on DoP

  I will start with the experts for an evaluation of DoP. This is C.A.R. Hoare, in the Foreword of DoP:

  The book expounds, in its author’s usual cultured style, his radical new insights into the nature of computer programming. From these insights, he had developed a new range of programming methods and notational tools, which are displayed and tested in a host of elegant and efficient examples. This will surely be recognized as one of the outstanding achievements in the development of the intellectual discipline of computer programming.

  When I spotted in 1976 a copy of DoP in the University of Waterloo’s book store, I pounced on it. Spurred on by this Foreword I decided to make that copy my own. On the basis of [4a] I looked forward to being able to derive alorithms from their specifications. After all, this article had only shown how to do it for the maximum of two numbers and for Euclid’s algorithm for the GCD. On closer inspection, WPs are mainly used in DoP to “semantically characterize” the guarded-command language.

  The first few chapters are devoted to Weakest Preconditions (here referred to as WPs), the guarded command language, and its characterization by WPs. Chapter 8, “The formal treatment of some small examples”, contains eight examples. The first seven are derived by means of WPs, and are trivial. The eighth example is neat: given its rank, find the permutation that has this rank. It is not derived. What EWD offers as explanation is interesting, but I failed to see a connection with the program. All I see is an intriguing bit of code of which I did not even begin to see how it would solve the problem. The easiest way to discover whether it was just nonsense, seemed to be to commit the ultimate sacrilege, to translate it to C. It passed enough tests to convince me of the original’s correctness.

  Chapters 13-25 are devoted to neat algorithms, one per chapter. I have only studied one, Chapter 17 on Hamming’s problem, well enough to reproduce a solution independently. Here EWD does a better job at explanation. Both the rank-to-permutation of Chapter 8 and Hamming’s problem effortlessly translate to C with a result that is hardly longer and not particularly inelegant.

  Although DoP does not make good on the promise of the title of [4a], it has compensating merits: it proves that the guarded-command language is a valuable invention: it is easy to learn and, thanks to it, EWD’s algorithms are accessible to me. This would not be the case if he had written them in Java, Python, or JavaScript. The neat algorithms, though not derived, are rationally motivated by presenting invariants that are found with plausible heuristics.

  5. The logic debacle

  In 1990 EWD published “Predicate Calculus and Program Semantics”, co-authored with C.S. Scholten” [5], here referred to as D&S. Egon Börger, a logician on the faculty of the Computer Science Department of the University of Pisa, wrote a review of D&S that appeared in The Journal of Symbolic Logic and in Science of Computer Programming [6]. It begins as follows

  The book deals with a fascinating subject, indicated in its title: a theory of program semantics based on predicate logic. When I was asked to write a review of this book, I was preparing a course on the subject and accepted with pleasure the opportunity to study what I expected to be an illuminating study from famous authors’ hands. Unfortunately, my expectation was not met. Moreover, I believe the book will not be helpful to those interested in the subject area. What follows is a detailed review that explains my critical judgement and the reasons I cannot recommend the book.

  What follows in Börger’s review seems to me a factual and somewhat technical account of some of the shortcomings of D&S.

  David Gries tried to be helpful and co-authored a paper that attempted to knock D&S into shape to make it palatable to logicians. EWD’s reaction is in “a semi-open letter to David Gries” (EWD1227). The following passage is relevant here:

  I never felt obliged to placate the logicians. I (kindly!) assume that their customary precautions are needed and sufficient for reaching their goals. If they can help and correct me by pointing out where my precautions have been insufficient and where my own discipline has led or will lead me astray, they are most welcome: I love to be corrected. (Besides being a most instructive experience, being corrected shows that the other one cares about you.) If however, they only get infuriated because I don’t play my game according to their rules, I cannot resist the temptation to ignore their fury and to shrug my shoulders in the most polite manner. (The other day I was shown—in Science of Computer Programming 23 (1994) 91-101 a Book Review by Egon Börger; it was a nice example of that fury.)

  It is puzzling that a matter-of-fact technical review is experienced as “fury”. That D&S is perhaps problematic to such a degree as being beyond review is suggested to me by another passage from EWD1227:

  I get completely confused as soon as logicians drag “models” and “interpretations” into the picture. I thought that the whole purpose of the creation of a formal system in which one can calculate was to create something independent of any model or interpretation.

  The story so far presents us with a puzzle: with the shortest path algorithm, the Algol 60 compiler, the creation of high-level concurrent programming primitives, and the THE operating system, EWD appears as a titan going from triumph to triumph. In each successive new field, it was “Veni, Vidi, Vici”. And then the debacle of D&S.

  I would like to offer the following explanation. Each of the triumphs occurred in virgin territory. If you are of EWD calibre, you can make a killing without the tedium of studying the literature because there is none. This was even true of the shortest path algorithm: although graph theory existed and had a considerable literature, the shortest-path algorithm is of interest as an instance of dynamic programming, which was in 1959 still too young to be required reading.

  6. Mitigating circumstances

  Until recently I only read the first paragraph of the Börger review, the one quoted above. I agreed: don’t buy this book. When I read further, my suspicion arose that there is more going on with D&S: it may not be just a badly written exposition of predicate logic. Badly written compared to what? What is predicate logic, anyway?

  Both questions have the same answer, D&S is badly written compared to the expositions in the textbooks by Patrick Suppes [7], Elliott Mendelson [8], Joseph Shoenfield [9], Herbert Enderton [10], and Andrzej Grzegorczyk [11], a random selection occasioned by my undirected course in logic. These texts describe the same logic: first-order predicate logic. These are written in such a way that I could read them—which was not the case with D&S. Why then did Börger not just dismiss D&S for what it seemed to be to me? Why did he find fault with D&S for not referencing work by I.I. Shegalkin and by H. Hermes, authors of whom I had never heard?

  6.1. Two varieties of predicate logic

  It turns out that there are two kinds of predicate logic: the kind unanimously described in the texts listed above, which I will call “mainstream logic” and an exotic kind, which Börger calls “boolean term logic”. I had no idea such a thing existed, but Börger, a logician, apparently recognized it as the kind of logic of D&S.

  If you are interested in boolean term logic, look elsewhere. But I will try to convey the sketchy idea of it that I picked up. The language of mainstream logic contains formulas and terms. The formulas assert relations that hold between individuals that are elements of a set called the universe of discourse. In the formulas the individuals are denoted by the terms of the language. A formula may be atomic, and then it consists of a predicate symbol and a smaller or larger number of terms, or it may be composed by means of connectives or quantifiers. A term may be simple, and then it is a constant or a variable, or it may be composed of a function symbol and a smaller or larger number of terms.

  The purpose of mainstream logic is to formalize axiomatic theories concerning individuals interest: numbers, or elements of other algebras such as semigroups, monoids, and rings; to mention some mathematical examples.

  This makes mainstream logic versatile: any set can be chosen as universe of discourse; any repertoire of function and predicate symbols can be chosen and any interpretation of these symbols can be chosen. Thus the universe of discourse can be infinite or finite. In the latter case it can consist of two truth values and the function symbols can be the operations of boolean algebra.

  This interpretation creates an intriguing situation. Each of the connectives that makes formulas out of simpler formulas is mirrored by the function symbol for the corresponding boolean operation. Inferences consisting of sequences or trees of formulas are mirrored by sequences or trees of equations between boolean terms. Though it seems to me an abuse of the versatility of mainstream logic, it is apparently sufficiently intriguing for logicians like Shegalkin and Hermes to investigate.

  So, the geniuses set out to discover logic from scratch, called it predicate logic, and it turns out to be the exotic variant. This is implausible, if one believes EWD’s official position that logicians have nothing of interest to tell him. If this is the case, then indeed there is a fifty/fifty chance of the coin falling one way (mainstream logic) or the other (boolean term logic). But if boolean term logic is what I think it is, then one must have some idea of mainstream logic to see that one can chose a domain for the variables that only contains truth values.

  But now the plot thickens. EWD wrote the Foreword to “The Science of Programming” by David Gries (Springer-Verlag 1981), here referred to as “SoP”. SoP develops “predicate logic” from scratch, without references. Which would be fine if it were the mainstream variety, but it is the exotic boolean term variety souped-up with specific programming-oriented constructs, like the conditional connectives can and cor. Consumer Reports would advise its readers to avoid such a homebrew concoction. EWD must have been both attracted and repelled by the logic of SoP, which could have led to D&S.

  Gries, a fan of EWD, understood that logicians would not approve of D&S, took the trouble to knock it into shape. Instead of being pleased and flattered, EWD issued a rebuke in the form of EWD1227.

  Börger may well have been correct in seeing no redeeming features in D&S. Yet I see mitigating circumstances.

  6.2. Dijkstra and Feijen

  WPs were introduced as an improvement on Hoare’s verification method by means of preconditions and postcondition. Not being aware of anything to the contrary, I assume that Hoare envisaged conventional predicate logic as the language for the assertions acting as pre- and postconditions. This works fine for individual variables, but it is not clear how to make assertions involving arrays: Hoare verification makes new demands on logic.

  An exception is “A Method of Programming” co-authored by EWD with Wim Feijen (1988, originally published in Dutch in 1984). This book has plenty of neat examples, typically involving arrays, all verified according to Hoare’s method, therefore all using predicate logic and handling arrays in a way worth paying attention to. I mention this to balance my critical remarks on DoP with this work that succeeds in everything it tries to do. Both DoP and Dijkstra/Feijen pay a great deal of attention to arrays. Having watched these struggles one can sympathise with those who want a clean break and start afresh with predicate logic.

  7. Advice in Consumer Reports style

  7.1. Don’t go for homebrew logics

  D&S is not the only example; in general computer people seem to have a penchant for whipping up homebrew logics. See E.F. Codd’s Relational Calculus [12], an obvious mess. I hope that somebody like Börger has reviewed the logic of SoP and the logic of D. Parnas (who allows functions to be partial) [12a], or will do so. In contrast, Alain Colmerauer is to be appreciated as a wise exception. When he needed logic, he got a logician, Robert Kowalski, as a consultant. As a result the programming language Prolog has a pure version that is logically impeccable.

  7.2. Don’t forget that logic is hard

  Predicate logic has a long history, one that goes back all the way to G. Frege in the 19th century. Many clever people worked on it and several came to grief. Frege was shattered when Russell presented him with the Barber Paradox. In the early 1930s A. Church published a version of predicate logic that is subject to the Kleene-Rosser paradox. Incidents like this motivated A. Tarski to create a logic with a model-theoretic semantics so as to be paradox-proof. Tarski’s work dates from early 1930s, but see the helpful exposition in his “Truth and Proof”, an article that appeared in 1969 in Scientific American. Further reason to be cautious with new systems of logic is the fact that W. Quine’s system in “Mathematical Logic” was claimed to be inconsistent by Curt Christian, whereupon the proof was claimed to be erroneous by Church. So, for a while at least, the jury has been out in this case.

  This history shows that when one wants to define program semantics by means of predicate logic one should be very careful. One way of doing that is to stick with the first-order predicate logic, mainstream variety, as presented by any of the undergraduate textbooks mentioned above. It is not only safer and but saves work compared to creating and publishing a homebrew system.

  8. The way ahead

  8.1. Lessons from the above

  The main lesson is to take a hard look at WPs. EWD used them to define the semantics of the guarded-command language. He also pointed out that binary relations are not adequate for such semantics because they do not capture the phenomenon that two non-deterministic programs may agree on all finite computations but one may have infinite computations while the other does not. WPs may be useful if they are the only way to make that distinction. If not, then best forget them, as I yet have to see a convincing example of their use to derive programs from postconditions.

  8.2. Hoare, but with assertions first

  If WPs don’t help in finding programs, what then? One can lower one’s ambitions from formally deriving programs to mere goal-oriented programming by Hoare’s method of informally proving partial correctness. But the development can and should be made goal-oriented by writing the postconditions before the code that is to ensure that they are satisfied.

  Although “A Method of Programming” by EWD and W. Feijen has the lowly status of course notes for an introductory course, it succeeds in presenting a convincing program development method, something lacking in DoP. That, and its assertions handling arrays with a logic of sorts, make D&F worth studying.

  8.3. Tweak predicate logic, gingerly

  But acknowledge that mainstream predicate logic offers no more than one-sorted logic with individual variables only. This is not adequate for writing assertions. A promising approach is “Formulas as Programs” by Apt and Bezem, [13], who propose to use predicate logic as programming language. They propose modifications of predicate logic that include arrays and multiple sorts for the variables. They manage to do this with minor modifications of mainstream predicate logic. It is encouraging that they do not belong to those who get

  completely confused as soon as logicians drag “models” and “interpretations” into the picture.

  In fact, they are logicians.

  Coda

  In my account so far, Structured Programming is just a term invented by EWD that caught on. It was widely interpreted as meaning programming without the goto statement. For EWD it meant a lot more. The year 1968, when the famous letter [14] appeared, marked a turning point in EWD’s career, witness the following quote from his retrospective EWD1308:

  In 1968 I suffered from a deep depression, partly caused by the Department, which did not accept Informatics as relevant to its calling and disbanded the group I had built up, and partly caused by my own hesitation what to do next. I knew that in retrospect, the ALGOL implementation and the THE Multiprogramming System had only been agility exercises and that now I had to tackle the real problem of How to Do Difficult Things. In my depressed state it took me months to gather the courage to write (for therapeutic reasons) EWD249 “Notes on Structured Programming” (August 1969); it marked the beginning of my recovery.

  His work in subsequent decades shows that he hoped that logic would help in solving the problem of How To Do Difficult Things. It turned out to be difficult to turn this hope into reality.

  Acknowledgements

  I am grateful to Paul McJones for discussions. This essay was propelled by Paul’s finding things, especially such gems as EWD1227. David Gries made several suggestions for improvement. Krzysztof Apt helped by pointing out my blind spot concerning self-stabilization and by making various suggestions.

  References

  [1] arxiv.org/abs/cs/0210001
  [1a] Philip Frana: “An Interview with Edsger W. Dijkstra”. Communications of the ACM. 53 (8): 41-47.
  [2] “Hints on Programming Language Design” by C.A.R. Hoare, Stanford Artificial Intelligence Laboratory, Memo AIM 224, December 1973.
  [3] Knuth, Donald E. “Structured Programming with go to Statements.” ACM Computing Surveys (CSUR) 6.4 (1974): 261-301.
  [3a] Dijkstra, E.W.: Self-stabilizing systems in spite of distributed control. Commun. ACM 17(11), 643-644 (1974)
  [3b] Apt K.R., Shoja E. (2018) Self-stabilization Through the Lens of Game Theory. In: de Boer F., Bonsangue M., Rutten J. (eds) It’s All About Coordination. Springer Lecture Notes in Computer Science, vol. 10865.
  [4] E.W. Dijkstra A discipline of programming Prentice-Hall, 1976.
  [4a] “Guarded commands, Nondeterminacy, and Formal Derivation of Programs” by Edsger W. Dijkstra, Communications of the ACM, vol. 18 (1975), pp 453-457.
  [5] E.W. Dijkstra and C.S. Scholten Predicate Calculus and Program Semantics Springer-Verlag, 1990.
  [6] Science of Computer Programming vol. 23 (1994) pp 91-101.
  [7] Introduction to Logic, D. Van Nostrand, 1957.
  [8] Introduction to Mathematical Logic, D. Van Nostrand, 1964.
  [9] Mathematical Logic, Addison-Wesley, 1967.
  [10] A Mathematical Introduction to Logic, Academic Press, 1972.
  [11] Outline of Mathematical Logic, Reidel, 1974.
  [12] “Relational completeness of database sublanguages”, Research Report RJ987, 1972. IBM Research Laboratory, San Jose.
  [12a] D.L. Parnas. “Predicate logic for software engineering.” IEEE Transactions on Software Engineering 19.9 (1993): 856-862.
  [13] K.R. Apt and M. Bezem. “Formulas as programs.” pp 75-107 in The Logic Programming Paradigm. Springer-Verlag, 1999.
  [14] E.W. Dijkstra “Letters to the editor: go to statement considered harmful.” Communications of the ACM 11.3 (1968): 147-148.