This month marks the 75 year anniversary of the publication of Alan Turing’s paper On Computable Numbers, with an Application to the Entscheidungsproblem. In that paper, Turing defined a universal computing machine, a theoretical construct capable of running programs. He didn’t set out to invent software. But that’s exactly what happened.

The Ensheidungsproblem

Turing’s goal was to show that there are statements in mathematics that are well-formed, but not decidable. That isn’t to say unprovable. That is to say that we can’t even decide whether a proof exists. This is an extremely important mathematical proof, but what is more revolutionary was the way in which Turing proved it.

Turing invented a machine that is capable of running programs. Each program prints out the digits 0 and 1, in addition to possibly doing some record keeping. A program is a finite series of instructions in a state transition table like the one above. If you “compile” the program, you will get an integer. It’s a really big integer, but it is finite. This lets you count the programs and put them in order.

Now, suppose that you had a program that would run all of these programs in order, but stop the n^th program when it prints the n^th digit. Would this program keep printing digits, like any good Turing program should? Or would it seize up?

If every program compiles to a finite number, then surely this program does too. Eventually, the program will run itself. When it does, it has already printed n-1 digits. It will run itself until it prints the n^th digit. But it never will!

Turing equated deciding whether a program gets caught in an infinite loop with deciding whether a statement is provable. Since we can’t evaluate a program to see if it will enter an infinite loop, neither can we decide whether an arbitrary statement is provable.

Modern day provability

These days, we have theorem provers, statically analysis, and code contracts that verify assertions about programs. And yet when Turing invented programming, he proved that these things could not work! Was Turing wrong?

No, Turing was absolutely right. These tools have limitations. There are some programs that you could write that these tools would not be able to prove correct. They won’t work in the general case.

But even though there is a vast infinity of programs that we cannot prove, there are plenty that we can. If we constrain ourselves to the provable set, then these tools can be of incredible value. Knowing where the boundary is helps us to get the most of these tools. And that is the true value of the Entsheidungsproblem.

Please read “The Annotated Turing” by Charles Petzold for a fantastic journey through this foundational paper. This is where our industry was born, only 75 years ago.