mbp speaks of the inability to prove that a program is free from bugs. this is broadly asserted, yet I feel a little twinge of annoyance every time I hear it, perhaps because it is so imprecise.

a bug is a subset of machine state space which you do not want to be reachable by implication from your program's text. a test is a single path through machine state space, either leading into a bug region (a test you want to see fail) or avoiding bug regions (a test you want to see pass).

there are far more possible tests than you can ever write or run, so you must choose "good" paths towards "important" bugs. the problem of a test writer is to determine which areas are important, and it can require deep insight into what the program is intended for.

but note: a bug, a test, and a program are all completely formal objects from this viewpoint.

a proof, on the other hand, is another formal object in a much larger "space" (a linguistic space in which machine state spaces, and some parts of your preferred maths or logics are basic terms). the sort of proof you are interested in is one which relates your program's text residing in memory at one point, to a (good or bad) region of machine state space which is implied by the program, via a logic whose rules you like.

any test can be translated into a proof in a silly logic easily: the proof is simply the trace of your processor executing your program's code on your test's input, and the logic is one in which each machine transition that happened is an axiom. but that proof is boring.

an interesting proof is one which is much smaller, when written down, than the sum of all the tests which you would need to write to fill the machine state space bounded by the proof. in this sense, I really believe Chaitin is onto something when he talks about proofs as nothing more than a form of "higher order data compression", and the value of a given formal system as the amount of compression it commonly admits over interesting data.

so, getting back to mbp's comment, certainly you can produce a very large set of (formal) bugs which nobody's compressed inside a proof yet, for any program you care to mention. but I do not think this means that all, or even a sizeable majority of those bugs will admit "no further compression" if the author puts their mind to it.

raph's suggestion that we design programs "the way we'd want to prove things about them" is, seen in this light, a suggestion that we design programs "in a way which admits a lot of compression". I think this fact is at the heart of the programmer aesthetic for "small and simple" programs. "larger" is often equivalent to "less provable", or similarly the feeling that any test you run explores too little of the state space to be helpful. you lose any confidence you have that a large system will do what you want, unless you can carve up the state space with type systems, modules, processes, etc.

as a final note: people often try to express test quality in terms of "code coverage", but this is only slightly useful, and less so as the quality of the program being tested improves. good programs parameterize much of their behavior on their input. their machine state space massively outweighs the size of their program text, so you learn very little about exercizable machine states by knowing that all the code was exercized.