dsimcha: > overflow Good provers take in account integral overflows too.
> rounding error Interval (floating point) arithmetic can be used to face a large part of this problem. I hope to see a good Interval arithmetic lib for D in few years. > compiler bugs > OS bugs Those software too can be proven :-) Microsoft is working on provable OS kernel. > hardware bugs You can use RAM with error correction, redundancy, etc. Proofs are one useful tool for high-reliability systems. They are not enough, of course. "Beware of bugs in the above code; I have only proved it correct, not tried it.'' -- Knuth Bye, bearophile
