jdybnis suggests that tests are worse than proofs; by failing to terminate they may make themselves hard to verify since their traces are infinite. I dispute this, since a test is often written within a testing framework which sets a timer and aborts the test after some time. I think tests, test-traces, and proofs are all finite formal objects, simply of varying scope.

mbp raises interesting points. first, that gcc and linux do not always fit common "specifications" of a C compiler and a POSIX kernel. this is worth complaining about, but is not a flaw in a proof of some formal properties of your distcc program, which treats the functions of kernel and compiler as axioms. as mslicker aptly quotes chuck moore: internal consistency can be proved, but compatibility can only be tested.

axiom testing is a different sort of "test" than I was talking about. surely one needs to test that the assumptions going into a proof hold in a particular environment, and those tests should indeed follow the scientific method of attempted falsification.

but I maintain that it's poor use of time to test a program in order to verify some static property you have a good formal theory of. consider gcc: running its larger testsuites takes hours-to-days. in all combinations of host * target arch, with all combinations of configuration flags, it would not finish before you die. and yet verifying the formal property that gcc is a syntactically valid C program, or that it is type-sound, or that every symbol used by a compilation unit has a definition in another, takes only a small factor more time than the i/o required to read it off disk. why is this?

it is because, unlike the (formal) property of "correct translation from C to machine code for architecture X", we have spent time and effort on some of the simpler properties (does-parse, is-typesound, uses-are-defined), and in the process developed the tools to state and verify them statically. applying gcc to other inputs ad nauseum, as a "test" that gcc is a syntactically legal C program, is a total waste of time. you check the static formal property once when the program text changes, and that's it. any more would only tell you that an assumption from the environment is wrong (disk i/o error?), not that the properties have changed.

davidw states that your competition will always outrun you if you bother to stop for proofs. this depends on how ambitious your proofs are; as I suggest above I think there are lots of properties we already prove, and many more waiting behind the scenes which we will have the opportunity to prove in the near future. will we reach a day when we can prove everything interesting about programs? certainly not. such a statement probably has no meaning. but it is instructive, from a business perspective, to consider how much time you spend running tech support, tracking bugs, debugging, issuing errata, etc. and compare it to the investment in various proof techniques. on several fronts, notably with customers who have deep pockets and long memories, I think the economics may favour "more proofs".

finally, mbp encourages me to try distcc, which is a very good suggestion; it's saved my life several times (though it only speeds up verification of formal properties, not the testsuites). fwiw, I'm your anonymous happy customer from june 4th :)