Why don't other programming languages have ranges?

[Don]

Jim Balter wrote:
> "Jonathan M Davis" <jmdavisprog at gmail.com> wrote in message 
> news:mailman.50.1280425209.13841.digitalmars-d at puremagic.com...
>> On Thursday, July 29, 2010 03:11:21 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.
>>
>> It's likely because the idea of being able to _prove_ that your 
>> program is
>> correct is rather seductive. As it is, you never know for sure whether 
>> you found
>> all of the bugs or not. So, I think that it's quite understandable 
>> that the
>> academic types at the least have been interested in it. I'd also have 
>> expected
>> folks like Boeing to have some interest in it. However, since it's so 
>> time
>> consuming, error prone, and ultimately not enough even if you do it 
>> right, it
>> just doesn't make sense to do it in most cases, and it's never a good 
>> idea to
>> rely on it.
>>
>> Given how computer science is effectively applied mathematics, I don't 
>> think that
>> it's at all surprising or ridiculous that correctness proofs have been 
>> tried (if
>> anything, it would be totally natural and obvious to a lot of math 
>> folks), but I
>> do think that that it's fairly clear that they aren't really a 
>> solution for a
>> whole host of reasons.
>>
>> - Jonathan M Davis
> 
> You've snipped the context; if you go back and look at what Don was 
> disagreeing with, it was simply that correctness proofs are *one tool 
> among many* for increasing program reliability -- no one claimed that 
> they are "a solution". The claim that they are "based on a total 
> fallacy" is a grossly ignorant.

No, I was arguing against the idea that they are a total solution. They 
were presented as such in the mid-80's. The idea was that you developed 
the program and its proof simultaneously, "with the proof usually 
leading the way". If you have proved the program is correct, of course 
you don't need anything else to improve reliability. I see this as a 
very dangerous idea, which was I think Walter's original point: you 
cannot completely trust ANYTHING.

I just have a big problem with the word "proof", because I feel it has 
connotations of infallibility. I also feel that of all the development 
methodology fads which arise periodically in computer science, this one 
did the least to improve program reliability throughout the industry.

BTW The idea pre-dated theorem solvers, which obviously improve 
reliability. I'm of course strongly in favour of static analysis tools.