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
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
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
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
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
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
graydon, you might like
distcc. It's somewhat similar
to your doozer
program, but perhaps a bit faster (in C, not Perl) and easier to
set up (it doesn't need a shared filesystem). (Or