Why don't other programming languages have ranges?

[Jonathan M Davis]

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