[FOM] Question on Axioms for FP-Arithmetic

[Steve Stevenson]

Did you look at all the work Kahan did in setting up the IEEE  
standard? His 'paranoia' program has all the properties in testable  
form but there's lots of groundwork starting in the 1950s. Or is that  
what you mean by "formal verification"? I don't understand why our  
need to verify that the computer is correctly working is "logic  
unfriendly". For those of us doing verification and validation of  
computer models, it is the world we live in.

Your proposal looks like interval arithmetic (also starting in the  
50s) to me and that is a very active community, too.

There are also very interesting models in the fuzzy, probabilistic  
world that are used in engineering.

Steve
--------
D. E. Stevenson, Department of Computer Science
Director, Institute for Modeling and Simulation Applications
Clemson University, Clemson, SC 29634-0974