Why don't other programming languages have ranges?

[BCS]

Hello Jonathan,

> 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 agree with you in theory but not in practice

In mechanical or civil engineering, yes there are huge amounts of very ill 
defined interactions and properties and in CS there are well defined abstractions 
that are very nearly ideal. However, most programs are written and debugged 
empirically; "if it runs all the test cases, it's correct". In the engineering 
disciplines OTOH, it is more or less required by law that a "semi-formal 
proof" be done for virtually ever aspect of a design (keep reading :). 

The procedure in a nut shell is; make a (mostly) formal statement of the 
success criteria, pick a bunch of (conservative) assumptions (general from 
well vetted research), and then formally show that under those assumptions, 
you have satisfied the success criteria. 

Now I will grant that (aside from the last step) this is a far cry from a 
formal math proof but in CS the success criteria is rarely more than informal 
and most projects doesn't even bother listing there assumptions, and rarely 
is there any proof, formal or informal, that the success criteria was met.

Ironic.

-- 
... <IXOYE><