checkedint call removal

[via Digitalmars-d]

On Thursday, 31 July 2014 at 11:32:11 UTC, bearophile wrote:
> A problem with code like this is that it's drowing in noise. 
> The precondition/invariant/variant code in the 't3' function is 
> obscuring what the code is actually doing on the data:
> http://toccata.lri.fr/gallery/queens.en.html

Yes, if the algorithm is a bit involved it becomes complicated. 
It is also expensive to get right, $100-$1000 per line of code?

However, simple stuff that you often have in a standard library 
is usually easier on the eyes and easier to get right:

http://toccata.lri.fr/gallery/power.en.html

So, having a formally proven standard library would be quite 
within reach. And if you also have inlining + assume() you could 
do stuff like this

inline uint floor_sqrt(long x){
    assert(x>=0);
    uint r = _proven_floor_sqrt(x);
    assume(r<=x*x);
    assume( (r>(x-1)*(x-1)) || x==0 );
    return r
}

Precompiled library:

uint _proven_floor_sqrt(long x){
    assume(x>=0); // not test necessary, use this for optimization
    return ...
}

Another nice thing is that you can replace _proven… with 
handwritten machine language that has been exhaustively tested 
(all combinations) and still let the compiler assume() the 
postconditions with no runtime cost.

Another area where assume() is useful is for reading hardware 
registers that are guaranteed to have certain values so no 
runtime check is needed:

auto x = read_hw_register(123456);
assume( x==0 || x==1 || x==4 );

> I have added a third version here:
> http://rosettacode.org/wiki/Dutch_national_flag_problem#More_Verified_Version

Thanks, I like the way you go about this. Experimenting with the 
syntax this way.

> D lacks the pre-state (old a) and (at a 'Init), the loop 
> variants, the loop invariants (despite D has a invariant 
> keyword used for struct/classe invariants),

Yeah, I also think having invariant() in loops makes for more 
readable code than assert/enforce.

I imagine that you could specify a reduced set of D and do this:

D-source => machinetranslate => prover-source

prover-source => prover => proof-source

proof-source + prover-source => machinetranslate => D-source 
w/assume() etc


Btw, here is an example of an open source operating system kernel 
vetted against a haskell modell of the kernel:

http://sel4.systems/
https://github.com/seL4/seL4/tree/master/haskell

So, this formal correctness support in one way or another is 
clearly a valuable direction for a system level programming 
language.