Why don't other programming languages have ranges?

Jim Balter Jim at Balter.name
Mon Aug 2 23:53:13 PDT 2010


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



More information about the Digitalmars-d mailing list