Geneva Talk



[Here are the contents of some visuals from Dijkstra's presentation in Geneva, 1973. Source: my archives, Box 11]

Our programs serve to instruct our machines.
-->   A “mismatch” is blamed on the program.

Our machines serve to execute our programs.
-->   A “mismatch” is blamed on the machine.

When a whole is considered as composed out of parts, the composition must define how the properties of the whole follow from the properties of the parts.
We therefore restrict ourselves to those ways of composing for which the above functional dependance is mathematically well-manageable.

We maintain a strict separation between “what something does” — its external properties — and “how something works” — its internal construction — .
{bottle full or drunk} empty the whisky bottle {drunk}
The initial condition “bottle full or drunk” guarantees that the action “empty the whisky bottle” cannot take place without causing the final state “drunk”.

In order to be convincing a proof must be reasonably short and straightforward.
shortness is achieved by the introduction of (suitable) “abstract data types” and “abstract operations”
straightforwardness is achieved by sticking to “sequencing disciplines” for which powerful theorems are known.

A concrete programming language can be translated automatically — i.e. without further human intervention — into (reasonably) efficiently executable code.
For an abstract programming language the translation is allowed to require further human assistance.
Abstract programs are indispensable stepping stones!