2 ms·
Believe it or not, people working on theorem proving are aware that computers use finite arithmetic, and they take this into account. Yes, floating-point comput
by tom_mellior 10y ago
Believe it or not, people working on theorem proving are aware that computers use finite arithmetic, and they take this into account. Yes, floating-point computations are hard and painful to verify. But no, it's not that easy to hand-wave away the whole field :-)
- aseipp 10y agoHonestly, it seems floating point computations are, by some measure, possibly pretty old at this point in the formal methods world! Intel has been investing in formal verification of its floating point units since at least the 90s when FDIV hit them, and this was when the tech was way worse than what we have today! Hell, CompCert -- which you can download today -- already has a proven adherence to IEEE-754 floating point, implemented by specifying IEEE-754 semantics in Coq, then using that to create a proof the compiler correctly preserves the semantics of IEEE-754 during the compilation process.