# How can one formalize and prove things about floating-point numbers, just as one can do with rational or real numbers?

Are floating-point numbers fundamentally different from the sets of rational or real numbers in any way? Are there any good mathematical treatments of floating-point numbers? Are they even interesting to study mathematically?

-

They are fundamentally different in that (given any particular floating-point representation) there are only finitely many of them. And the basic arithmetic operations on floating-point numbers do not satisfy nearly as many nice laws as arithmetic on true reals or rationals do -- for example, $(a+b)+c = a+(b+c)$ is not true for floating point; neither is $(a+b)-b = a$.
If you use a finite number of bit, you have the same problem as above: $a=1$, $b=1*2^{64}$. $a+b=1*2^{64}$ (or use higher exponent if you have higher precision number). $(a+b)-b=0$, but $1\neq0$... – carlop Apr 24 '12 at 0:52