Saturday, May 3, 2008

Halting Taboo

There are limits people are comfortable with. No one would suggest that you could go faster than light, or that ignoring the second law of thermodynamics may be a good idea.

Unfortunately, when it comes to problems a computer can't solve, undecidability can prove to be a misunderstood, if not downright unpopular, limit.

For instance, it is impossible to write a program that receives an arbitrary program as input and determines if it stops in a finite amount of time. This is known as the Halting Problem; in the 1930's Alan Turing proved that it isn't decidable. [1]



If you can't programatically decide if a program stops, automated tests can't prove that it has no bugs. Surprisingly, say it aloud,

You can't prove that a program is correct.


and the conversation can turn sour. "Of course it can be done, you test every state, even if it takes months or years. We are talking about real machines!"

How do you know if a program isn't stuck in an infinite loop? Besides, even if the number of states is finite, it can be huge. Testing every possible state is not feasible.

"Ok, but you're forgetting about formal methods."

Formal methods are applied to individual algorithms, written in pseudo-code. The running program is a different beast. I think it is no coincidence that Knuth once said:

Beware of bugs in the above code; I have only proved it correct, not tried it.


Software is hard. There are lots of descriptions of things going wrong. It is not like catastrophic failures are unheard of. Why the state of denial?


Notes:

[1] Incidentally, Turing used a diagonalization argument to construct his proof by contradiction. This technique was previously used by Cantor to show that the set of the Reals is uncountable (there are many different infinites). Gödel used it to prove his famous incompleteness theorem.

No comments: