Why you cannot prove software correctness: report from QCon London

I’m at QCon London, an annual developer conference which is among my favourites thanks to its vendor-neutral content.

One of the highlights of the first day was Tom Stuart’s talk on impossible programs. Using a series of entertaining and mostly self-referential examples, Stuart described why certain computing problems are uncomputable. He also discussed the “Halting problem”: unless you emasculate a computing language by removing features like While loops, you cannot in general answer the question “will this program ever finish”.

All good fun; but the dark side of the talk comes at the end, when Stuart proves with a flourish that a consequence is that you cannot prove software correctness.

In a world that is increasingly software-driven, that is a disturbing thought.

One thought on “Why you cannot prove software correctness: report from QCon London”

  1. While it’s part of Turing’s proof that due to the halting problem there can be no algorithm / methodology that proves whether an algorithm halts, it can very well be that a given algorithm A can be proven to halt/not halt given input I. The main problem is of course that one has to do this manually, for each algorithm, as, due to the halting problem, there’s no general solution which can be applied everywhere. One could eventually use approximations, like which are used in e.g. whether a piece of code is unreachable or not. It’s not as black/doom as it might have made out to be, however indeed if people were hoping for a general ‘run this to check whether your software is correct’ then they will be disappointed. 😉

Comments are closed.