A science of logical machines

When Edsger Dijkstra started to write his book on a computer science course, he intended to define a more strict formulation for the study of algorithms. In this view, programs should be thought as logical mechanisms whose behavior and properties can be studied without awareness of any mechanical implementation.

Programming without computers

A computer doesn’t know about the program it’s executing. The logical goal of the application is completely hidden to the machine: not even the meaning of a single variable or operation. All the computer ‘sees’ (if we imagine there is ‘something’ operating the computer) is a static configuration of its memory which will be manipulated according to its internal mechanism. The brush isn’t aware of the painting, the work can be enjoyed only by a sensibility that dresses the colors and shapes with interpretation (don’t take it as a direct analogy, as the author remarked often, analogies can obscure instead of clarify). Program functionality can only be ‘used’ in the context of a system that interprets ‘embodied’ mechanical behavior, being that a user, a client application, etc. The end of chapter 0 - Executional abstraction remarks that an algorithm is the logical design that defines a type of computation:

An algorithm embodies the design of the class of computations that may take place under control of it

Is in this context that Dijkstra tosses away the execution medium in favor of the logical, abstract medium as the place where general computations are formulated. Indeed, the first chapter remarks that a program’s essential feature is the formulation of a general solution to a class of problems. The ability of an environment to perform computations that implement such a formulation is a (lucky) coincidence. The truth is Euclid did not need a mechanical automaton to formulate the algorithm that finds the greatest common divisor of two numbers: he only had to pose a set of rules and prove they generalize to any pair of positive integers based on properties common to all. In that sense, the logical mechanism has the advantage of operating over abstract objects suitable to the abstract problem: the soundness of the mechanism rest over a small set of assumptions. In the case of Euclid’s algorithm, one would need to assume a computing entity which is capable of (or whose behavior can be interpreted as implementing) arithmetic operations, persisting two integer values, making comparisons, movement from one operation to another, etc. If we take these for granted, the logical soundness of the following argumentation guarantees the completeness of Euclid’s formulation (for any element scoped to the definition of the problem):

For two integers X, Y greater than 0 and less or equal than 500, compute their greater common divisor:
1. Let the pair (x, y) be integer values assigned to the simbols (&x, &y). Initially, (x, y) = (X, Y).
2. If x = y, the procedure terminates with result GCD(X,Y) = x.
3. If x < y, assign to &y the value y - x, in other case, assign to &x the value x - y
5. Redo step 2

The algorithm travels through (x, y) pairs, and terminates when x = y. Then, the completeness of the program lies on a small set of arguments:

If (x, y) is any of the 249,500 points not on the answer line and (x', y') is the point to which the pebble will then be moved by one step of the game, then either x' = x and y' = y - x or x' = x - y and y' = y. It is not difficult to prove that GCD(x, y) = GCD(x', y')(…)

Secondly-and again it is not difficult- we can prove for any point (x, y) where x = y (…) that GCD(x, y) = x(…)

Thirdly -and again this is not difficult- we have to show that for any initial position (X, Y) a finite number of steps will indeed bring the pebble on the answer line.

(The provided arguments reference a possible embodiment device: a game that directs the movement of a pebble over an enormous grid that contains every possible position (x, y))

Another device to implement Euclid’s algorithm

Sound program design

Taking this frame of reference, programming languages are but formal notations to describe abstract operations. Their main virtue is to provide a reference system to compose powerful formulations that only occasionally will run on a computer. This view is shared at the end of chapter 1 - Role of programming languages:

I view a programming language primarily as a vehicle for the description of (potentially highly sophisticated) abstract mechanisms. As shown in the chapter "Executional Abstraction", the algorithm's outstanding virtue is the potential compactness of the arguments on which our confidence in the mechanism can be based.

This prior confidence in a system function is the reason these ideas are as crucial as ever to software engineering. The increasing complexity and growing scope of modern software require the development of techniques to anticipate the soundness of a system design independently from any technology or infrastructure implemented. Reading these pages published as early as 1976, one can envision the creation of system scoped languages (such as the promising TLA+ modelling language by Leslie Lamport) and development environments around formal properties and the patterns that emerge from them. This is, of course, easier said that done.

Coming soon: chapters 2 to 4.

[1] E. W. Dijkstra, A Discipline of Programming, Prentice-Hall, 1976.