Why don't other programming languages have ranges?

Don nospam at nospam.com
Thu Jul 29 12:34:35 PDT 2010


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.


More information about the Digitalmars-d mailing list