Reiner Pope Wrote:
> > If you don't isolate the in/out tests from the body, a proof by induction couldn't know what needs to be proved to prove the code safe.
> I agree with how you would code it here, although I wouldn't expect the compiler to verify all my conditions at compile-time.

I agree m8.  It should be a separate feature and/or program that you run when your program compiles and you want to make it proveably correct (bug-free)

> To me, the point about the 'in' contracts is that they will only ever trigger at a bug.

To me, bug = failure.  As programmers, we often accept six dozen failures in a program without realizing it and then find out 7 years down the road (see the libc quicksort bug).  If we could have a tool to help us completely eliminate bugs, wouldn't that be awesome?  Contract programming *allows* us to, it doesn't by default though.

> You hope not to have any of these when you release, so you are spending unnecessary processing time checking things which should always be true anyway.
> 
> If there is a bug, then either way you get a crash for the end user; an assert failure isn't really so much more pleasant than a segmentation violation for an end user.

Not always, sometimes it just gives you no answer, or worse, the wrong one.  Sometimes it works for all cases but exactly one number, which means you find it years and years down the road and a 38million dollar system crashes because of it.  Picture if that was how the libc quicksort bug was found... libc is thought to be stable.

> Such a program would surely be very useful, but I'm not convinced it should be done through compile-time programming (automated theorem proving takes a long time: you wouldn't want to run it *every time* you compile, and you also wouldn't want to run it through CTFE, which is slow).

It only has to parse and maintain a set of possible min/max pairs.  I'm suggesting it would be possible to prove by induction for non-constants and constants alike; by examining how they are modified through possible program flows, and verifying that by the time they hit an "in" or "out" they are within acceptable parameters.

This would be done by reverse-tracing the potential flow paths up to the declaration of the variable, and then doubling back fetching possible ranges going back down each of those potential flow paths to the result.  This has a marked similarity to chess algorithms.

Dumping the potential program paths, performing spectral analysis and such would be well beyond the scope of what most programmers are used to.  However, I feel with sufficient development it could become almost completely automated.

It would also formalize and automated what most senior programmers already try to do in their head.

> 
> If anyone is interested, though, Sage (http://sage.soe.ucsc.edu/) and Spec# (http://research.microsoft.com/specsharp/) are research languages which attempt to statically verify as much in the contracts as possible.

Ooo... sweet.  Something *interesting* to read.

> 
> Cheers,
> 
> Reiner

On that note, Walter, any chance we can get access to the AST?