Mission:Impossible:II - Will it ever Stop?

A problem that badly needs to be solved is how to be sure whether computer programs work properly. There have been a whole catalogue of famous cases where a program that the programmers believed to work, turned out not to in some obscure situation that happened in reality not to be that obscure. Terry Pratchett's old adage holds firm in the software world

There are lots of examples of software bugs leading to devasting consequences. Telephone systems have ground to a halt, space ships have exploded, cancer therapy machines have killed the people they were trying to save. Even when the computer bugs have not hurt people they have cost billions of pounds worth of damage.

What's the problem? Are programmers just careless? Don't they check the programs work? That's the problem. Programs are so complex, it is impossible to check every possible situation it could get into. There are just too many possibilities.

What we really need is a computer program that will check other programs and say whether they do what is intended. In fact very many computer scientists are working on just that: such tools are known as software verification tools. The idea is to build a program that is given the text of another program and a description of what it is supposed to do. The checking program then says whether it does what is described using mathematical proof rather than testing all the possibilities. Big corporations are pouring money into this approach and it is starting to pay dividends.

Turns out, though that this is another one of those Mission:Impossible tasks. It has been proven that it is not possible for a program to exist that can unfailingly tell you whether any program it is given is correct or not. In fact, it's worse than that. No program can exist that can even tell you whether any program it is given will always stop or not, never mind give correct answers. This is one of the most famous problems in computer science and is known as "The Halting Problem".

So was Bill Gates just joking? Has Microsoft now hired the Mission Impossible team? Well no, and they aren't the only ones building tools that can check whether programs work or not - in fact people have been doing it for 50 or more years. So what is going on? The point is that such verification tools can exist. The halting problem just says they can never be perfect. There will always be some program they either give the wrong answer or no answer for. That doesn't stop them being really useful for lots of other programs. Software verification is still a hard problem though and the race is on to improve such checking tools so they catch more and more problems for bigger and bigger programs.

So remember, next time your computer crashes, it's an impossible problem even to prove it will ever stop, but computer scientists are on the case.