In the very same stroke wherein he created the computer program, the architect declared that it cannot be verified.

Alan Turing set out to prove that some problems are undecidable. Not that they don't have a solution -- Kurt Godel proved that several years earlier. No, Turing proved that you cannot even decide whether or not they have a solution.

To do so, he created a keyboard. On this keyboard were symbols that represented operations that a machine could perform. A programmer would sit at this keyboard and enter a string of symbols onto a tape, leaving spaces in between for a Universal Turing Machine to use as a workspace. The Universal Turing Machine was capable of executing any program that the programmer was clever enough to enter using the keyboard that Turing provided.

Now enter an observer. The observer would like to know whether the program meets some set of requirements. Take a simple requirement: that the program print a zero. Sure, it would be easy to write a program that satisfies this requirement, but the observer doesn't get to write the program. He is simply given a program, and he has to decide whether or not it prints a zero. The programmer could type anything at all on Turing's keyboard.

If the programmer typed "Print 0", then the observer would declare the program correct. If the programmer typed "Print 1", then he could declare it incorrect. But he could just as easily type convoluted branching logic with a "Print 0" embedded within. If the observer were unable to follow the branching logic to completion, he may find it difficult to discover whether the embedded statement is ever executed. Turing showed that there are some programs that could be written, where the observer would not be able to decide.

Decidable Programs

So if we cannot even prove this simple assertion about an arbitrary program, what hope have we of more interesting assertions? How can we prove, for example, that a banking program does not create or destroy money? How can we prove that a communication program opens a connection before sending a message? In short, how can we prove that our software has no bugs?

There is only one way. We need only take Turing's keyboard away from the programmer.

Let us not allow him to enter any arbitrary sequence of instructions. Instead, let's confine him to a small set of transforms. He must start with an empty program. Then, to achieve a single requirement, he must transform the program by following a constrained set of rules. He must transform the program step-by-step into a more complex construction that eventually solves all given requirements. At each point along the path, the program is verifiable. We never let the programmer stray into the space where the program is undecidable. There are certainly some programs that cannot be written this way. But if we are careful in our selection of transforms, then perhaps we can write most of the interesting ones.