The Origins of Formal Methods

One of the key events in the early development of formal methods was T. J. Dekker's invention of his mutual exclusion algorithm, not so much because of the practical value of the algorithm, which is rather limited, but because of the way Dekker developed it. Edsger Dijkstra tells the story in EWD 1303:

For economic reasons one wants to avoid in a multiprogramming system the so-called "busy form of waiting", in which the central processor is unproductively engaged in the waiting cycle of a temporarily stopped program, for it is better to grant the processor to a program that may actually proceed. This economic consideration was in 1961/62 a strong incentive for the introduction of the P/V-synchronization mechanism, which made it explicit to the scheduler when a program was no candidate for processor time. An in retrospect more profound incentive, however, came from an experience I had in 1959 at the Computation Department of the Mathematical Center in Amsterdam.

I had invented what, in that environment at least, was a new type of problem. Consider two cyclic processes, each consisting of an alternation of "a critical section" and "a noncritical section". Was it possible to synchronize these two processes such that at any moment at most 1 of these processes would be engaged in its critical section? The way in which the processes could communicate was by atomic reads and writes in a common store. After having convinced myself that --at least according to the State of the Art of those days-- the answer was not obvious, I broadcast the problem to the members of the Computation Department for their general amusement and distraction. It was given that each execution of a critical section would only take a finite amount of time and it was required that a process ready to execute would in due time get the opportunity to do so.

Many purported solutions were handed in, but on closer inspection they were all defective, and my friends realized that the problem was harder than they had suspected and that their simple "solutions" wouldn't do. Fortunately my friends didn't give up and they handed in "improved" versions of their earlier efforts. But as their designs became more and more complicated, it became harder and harder to construct a counterexample. I couldn't keep up with them and had to change the rules of this programming contest: besides a program I required a proof that the program had all the desired properties.

And then something profound and lovely happened. By analyzing by what structure of argument the proof obligations could be met, the numerical mathematician Th.J. Dekker designed within a few hours the above solution together with its correctness argument, and this settled the contest.

Proof-driven development back in 1959!  Much of Dijkstra's subsequent work can be seen as working out the consequences of the insight that programs should be developed with proof in mind.