Jérôme M. Berger wrote:
Don wrote:
I have to disagree with that. "Correctness proofs" are based on a total
fallacy. Attempting to proving that a program is correct (on a real
machine, as opposed to a theoretical one) is utterly ridiculous.
I'm genuinely astonished that such an absurd idea ever had any traction.
The idea isn't absurd, but you need to use it properly. Saying "I
have run a correctness prover on my code so there aren't any bugs"
is a fallacy, but so is "I have run unit tests with 100% coverage so
there aren't any bugs". The point of correctness proofs isn't that
they will find *all* the bugs, but rather that they will find a
completely different category of bugs than testing.
So you shouldn't run a correctness prover on your code to prove
that there aren't any bugs, but simply to find some of the bugs (and
you can find a lot of bugs with such a tool).
Jerome
You can certainly catch bugs with that technique, but the word "proof"
has no business being there. It's like the "unsinkable" Titanic.
(I think it's really similar, actually. Apparently the only reason the
Titanic sank was that many of the rivets were defective).
My recollection from university courses was not that "proofs will find
bugs in your programs". Rather, it was that "proofs will ensure your
program is correct".
The reason I think it's absurd is that (AFAIK) no other modern
engineering discpline has attempted to rely on correctness proofs.
