[FOM] Question on Axioms for FP-Arithmetic

Steve Stevenson steve at cs.clemson.edu
Wed Sep 17 11:13:49 EDT 2008

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.

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

More information about the FOM mailing list