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.