sorry to hijack the discussion but do you see any chance of consolidating the theoretical framework of real numbers with practical calculations of floats?
That is if I proof the correctness of some theorem for real numbers ideally I would just use that as the algorithm to compute things with floats.
also I was shocked to learn that the simple general comparison of (the equality of) two real numbers is not decidable, which is very logical if you think about it but an enormous hindrance for practical applications. Is there any work around for that?
You can use floats to accelerate interval arithmetic (which is "exact" in the sense of constructive real numbers) but that requires setting the correct rounding modes, and being aware of quirks in existing hardware floating point implementations, some of which may e.g. introduce non-exact outputs in several of the least significant digits, or even flush "small" (for unclear definitions of "small", not always restricted to FP-denormal numbers) results to zero.
Equality is not computable in the general case, but apartness can be stated exactly. For some practical cases, one may also be able to prove that two real numbers are indeed equal.
also I was shocked to learn that the simple general comparison of (the equality of) two real numbers is not decidable, which is very logical if you think about it but an enormous hindrance for practical applications. Is there any work around for that?