Why don't other programming languages have ranges?

[BCS]

Hello Don,

> 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".

I think the best a correctness proof can do is assert that, under a set of 
assumptions (including things like the machine working correctly) the program 
will do certain things and will not do certain things. E.g. all memory allocations 
have exactly one owner at all times and nothing is ever de-allocated that 
is an owner of anything.

There are several issues with this: First that it can't be proven that the 
things the program will and will not do are the correct things. Also, it 
is very costly ( >1 man/year per kLOC)

> The reason I think it's absurd is that (AFAIK) no other modern
> engineering discpline has attempted to rely on correctness proofs.
> 

Every engineering discipline I have any experience with gets a heck of a 
lot closer to producing formal proofs of correctness than programing. (BTW: 
I don't consider CS as generally practiced to be an engineering discipline.)


-- 
... <IXOYE><