Hello dsimcha,
Yea, here's a laundry list of stuff that theory doesn't account for
that can go wrong on real machines:
overflow
Theory can
rounding error
Theory has:
A mechanically checked proof of the AMD5K 86 floating-point division program:
http://ieeexplore.ieee.org/Xplore/login.jsp?url=http://ieeexplore.ieee.org/iel4/12/15456/00713311.pdf%3Farnumber%3D713311&authDecision=-203
Any proof that fails to take those into account is flawed.
compiler bugs
hardware bugs
OS bugs
OTOH A proof might be able to derive a unit test that will find most relevant
bugs
I sincerely wish all my numerics code always worked if it was provably
mathematically correct.
--
... <IXOYE><
