My diary on what Dijkstra did in the 1980s.

Picture on the right: Edsger and his student Netty van Gasteren sitting behind Edsger's desk in his home in Nuenen. Notice the two telephones.

My diary on what Dijkstra did in the 1980s.

Picture on the right: Edsger and his student Netty van Gasteren sitting behind Edsger's desk in his home in Nuenen. Notice the two telephones.

Submitted by egdaylight on

26 July -- 10 August, 1981

The theme of the International Summer School in Marktoberdorf was "Theoretical Foundations of Programming Methodology". The general pattern of the day was: two lectures — a break — two lectures — lunch — two lectures — break — discussion.

In his trip report, Dijkstra listed several speakers from that summer school:

Submitted by egdaylight on

19-25 July 1981

About 65 participants, including Dijkstra, attended the "Advanced Course on Functional Programming and its Applications" at the University upon Tyne (20-31 July 1981). The following points are of general interest because they seem to have recurred throughout Dijkstra's career:

Submitted by egdaylight on

21 May 1981

Dijkstra's Structured Programming abided by a top-down presentation of his programs. In the Spring of 1981, Van Gasteren and Dijkstra recommended a similar presentation style for mathematical arguments. For instance, they advocated using lemmata before giving their proofs:

Though unusual, this seems entirely correct. The statement of a lemma is a logical firewall between its usage and its proof; the use of a lemma is independent of how the lemma can be proved and, during study of its use, knowledge of its proof is therefore an unnecessary burden. [AvG5/EWD788 - 5]

Submitted by egdaylight on

21 May 1981

Using the right notation is key to proving theorems elegantly. To get this message across, Van Gasteren and Dijkstra explained why they were dissatisfied with the notation that Courant and Robbins had used in a particular proof concerning the prime decomposition of a natural number m. The notation under scrutiny was:

Submitted by egdaylight on

21 May 1981

In the Spring of 1981, A.J.M. van Gasteren and E.W. Dijkstra wanted to understand "how to tame the complexity of artefacts such as proofs and programs". In hindsight it is no surprise that Dijkstra's rallying cry for generalization in programming of the early 1960s is reflected in his work of the early 1980s with regards to proving mathematical theorems. Some examples below will illustrate this, based on AvG5/EWD788.

Submitted by egdaylight on

19 May 1981

On 19 May 1981, Dijkstra spent the day in Munich with Bauer, Broy and Partsch in order to select the participants for the NATO Summer School in Marktoberdorf [EWD790]. It is interesting to note how close Dijkstra and Bauer had become by 1981.

Submitted by egdaylight on

23 April 1981

At the Computing Laboratory of the University of Kent, Dijkstra lectured on semantics preserving program transformations (cf. EWD776).

Submitted by egdaylight on

15 March 1981

Though Dijkstra's own research publications were cited a lot, he himself did not want to judge the quality of one's work in terms of number of citations, nor in terms of number of papers.

Submitted by egdaylight on

28 February 1981

In a letter to Nils J. Nilsson, Dijkstra expressed his misgivings about research in artificial intelligence (AI). Only automatic theorem proving deserved his appraisal. (EWD778)

Submitted by egdaylight on

8 February 1981

Given a specific function, called lambo, how do you prove that it is equal to its own inverse? Dijkstra's answer: by massaging a program that computes lambo. That is, by gradually transforming an original program that computes lambo into a symmetric program that is rather useless to the programmer but useful to the mathematician!