The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Tue, Dec 9, 2014 at 2:03 AM, Thorsten Altenkirch <Thorsten.Altenkirch AT nottingham.ac.uk> wrote:

Yves makes a very good point: All the functions from the Reals to Bool are
constant because all computable functions are continuous. This clearly
limits very much what we can do with real numbers, they are a bit of a
³black hole² as far as information is concerned.

I think you mean any computable, *well defined* function from the reals is continuous.  It's easy enough to write a function which e.g. takes an approximation of the input to six decimal places, and returns true if the approximation is within 10^-5 of zero.  I think that's one sort of thing that numerical algorithms tend to do - check if some result is within some epsilon of zero, or within some epsilon of being positive, etc.  Sure, in the boundary cases that will tend to goof up, but you try to arrange things so that the algorithm works correctly in the "generic" case.

-- 

Daniel Schepler