[FOM] Question on Axioms for FP-Arithmetic
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