Seeing is deceiving. It's eating that's believing. -- James Thurber
I'm surprised by graydon being annoyed at the statement that it is impossible to be completely sure that a program is completely free of bugs.
graydon describes bugs as being states that we do not want to reach, and he suggests that we can do proofs to demonstrate that the program does not reach them. I agree that this is useful, however: (a) proofs alone cannot demonstrate that a program will not reach a bug state, and in fact (b) nothing can demonstrate that beyond doubt.
We always have an imperfect understanding of the way our system will behave in the real world. Therefore we are not able to completely identify ahead of time which states ought to be considered bugs, let alone which bugs are most important.
For distcc, I've tried to make a good effort at both demonstrating ahead of time that the design would work, and also at testing it thoroughly. However, during the course of testing I discovered a kernel bug and an undocumented behaviour in gcc, amongst other things. distcc has a bug because it needs to work around these limits.
These are states which turn out to be bugs but which were initially believed not to be. Unless we make unrealistic assumptions of omniscience, then really I don't see how these could have been discovered other than through testing. (This is even more serious in Samba, where the protocol it's meant to perform is undocumented and very complex.)
Let me try to state it more precisely. Represent our program as a function f(i) => o from input to output -- for interesting programs, the input and output will be large ensembles of values, and so are astronomical in number. Now define a correctness function cf(i), which is true for inputs where f is correct.
The proposition P is that "there are no bugs in program X", which is to say that for every i, cf(i) is true. As I understand it, Popper's point of view is that we cannot ever be sure that we have proved P is universally true. There are too many inputs to examine them all, and if we make a theoretical argument it may be flawed, or it may not correspond to reality. Some people disagree with him.
Rather than trying to gain confidence by piling up evidence in favour of P, Popper says that it is better to try hard to falsify it, either by finding inputs for which is is not true, or by showing that P is internally inconsistent. Considering formal description of f is one good way to find ways in which it is not always correct.
Popper describes science as a stepwise process of formulating theories and then trying to falsify them. This seems broadly like the way people do software. However, perhaps we can do better science by making programs which better support falsification by either tests or proofs. For example being well factored, well documented, and deterministic helps both approaches. Popper's results don't stop us finding scientific theories that are both useful and also almost certainly true. Similarly, never being absolutely sure that a program is bug free ought not to discourage use from developing good software and being appropriate confident in it.
Every year in developing countries, a million people die from urban air pollution and twice that number from exposure to stove smoke inside their homes. Another three million unfortunates die prematurely every year from water-related diseases. [The Economist]
Wow. (Yes, I am taking those numbers with a grain of salt, and yes, everybody has to die of *something*, but still.)
giants, shoulders of