Page "Edsger W. Dijkstra" Paragraph 8

From the 1970s, Dijkstra's chief interest was formal verification.

The prevailing opinion at the time was that one should first write a program and then provide a mathematical proof of correctness.

Dijkstra objected noting that the resulting proofs are long and cumbersome, and that the proof gives no insight on how the program was developed.

An alternative method is program derivation, to " develop proof and program hand in hand ".

One starts with a mathematical specification of what a program is supposed to do and applies mathematical transformations to the specification until it is turned into a program that can be executed.

The resulting program is then known to be correct by construction.

Much of Dijkstra's later work concerns ways to streamline mathematical argument.

In a 2001 interview, he stated a desire for " elegance ", whereby the correct approach would be to process thoughts mentally, rather than attempt to render them until they are complete.

The analogy he made was to contrast the compositional approaches of Mozart and Beethoven.