Formal theory on floating point numbers? Is there a formal theory involving the set of floating point numbers? Like topological properties, analytic properties, etc. There's no abstract theory involving floating point set? I usually find a lot of stuff in engineering strictly related to implementation, but nothing in terms of abstract theory.

You might be interested in section 4.2.2, "Accuracy of Floating Point Arithmetic", in The Art of Computer Programming, Volume 2, Seminumerical Algorithms, Third Edition by Donald Knuth, especially subsection A., "An axiomatic approach".  Knuth shows how to reason logically about floating point arithmetic.
