Why don't other programming languages have ranges?

[Jonathan M Davis]

On Thursday, July 29, 2010 12:34:35 Don wrote:
> The reason I think it's absurd is that (AFAIK) no other modern
> engineering discpline has attempted to rely on correctness proofs.

Really, the reason that you even _can_ attempt such proofs is because computer 
science is effectively applied mathematics. No other engineering discipline is so 
purely mathematical. They have have to deal with real world physics, so while 
they could undoubtedly prove _some_ stuff about what they do, it's not like you 
could ever prove something like your bridge will never collapse. Best case, you 
could show that it wouldn't collapse under certain types of stress. And since 
what you're doing is so thoroughly rooted in the physical world (with it being a 
physical structure built out of physical materials), it really doesn't make much 
sense to try and prove much about since that would all be rooted in theory.

Computer science, on the other hand, being thoroughly rooted in mathematics and 
generally having very little with physical reality allows for such proofs - even 
begs for them in at least some cases because that's the sort of thing that you 
do in math. However, even if you are able to correctly do such proofs, programs 
have to run on a physical machine at _some_ point in order to be worth anything, 
and then many of the assumptions of such proofs fall apart (due to hardware 
defects or limitations or whatnot). Also, it's not all that hard for a program 
to become complex enough that doing a proof for it is completely unreasonable if 
not outright infeasible.

I'd be tempted to at least consider proofs as _one_ of the steps in ensuring a 
correct and safe program for something like a plane or the spaceshuttle where 
the cost of failure is extremely high. But relying on such proofs would unwise 
(at best, they're just one of the tools in your toolbox) and the cost is 
prohibitive enough that there's no point in considering it for most projects.

Proofs are mainly used by academic types, and you're really not likely to see 
them much elsewhere. They're just too costly to do, and actually proving your 
program correct only gets you so far even if you can do it. That's probably a 
good chunk of the reason why the only time that you've really run into such 
proofs are with academic types interested in proving program correctness for the 
sake of correctness rather than programmers looking to use it as a tool to help 
ensure that they have safe and properly debugged code.

So, personally, I don't think that they're absurd, but it is unwise to rely on 
them (particularly when it's so easy to get them wrong), and most of the time, 
there's no point in dealing with them.

- Jonathan M Davis