The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

On 02/10/2015 03:37, Abhishek Anand wrote:
> More generally, in "type theory" (at least in Coq), to be able to reason
> about something, it must be well typed (AFAIK).
> So, if one insists that there be no well-typed approximation function, I

No, it is not that there is no well-typed approximation function. It is
that there is no well-typed approximation function that is built using
arithmetic operators over properly quotiented reals, even if they are
constructive.

But you can well have two separate types R (for quotiented real numbers)
and Q -> Q (for approximation functions) with operators defined on both
of them. You can then define arithmetic operators on both sets with
functions that are almost syntactically equivalent (they would be, if
not for the quotient used when defining R). This syntactic equivalence
makes proving the adequation of the approximation functions with the
real ones trivial. (But that would not guarantee anything about
performances, see below.)

> don't see how one will be  able to reason about a large class of useful
> functions which need to perform such approximations.
> I have to not only run the robotic programs, but also to reason about
> them, e.g. prove safety or liveness properties.
> 
> The robot application is just one among several ones. 
> I think we should have a Matlab/Mathematica based on constructive reals,
> and proved correct at least to some extent.

Having Matlab and Mathematica proved correct would be great. But
implementing them on top of constructive reals, would it be that great?
Sure, that would make proving them correct much easier. But they would
no longer compete with other computer algebra systems performance-wise.
Just because you need real numbers to specify and prove the correctness
of an approximation algorithm does not mean that you have to use real
numbers when designing such an approximation algorithm. That would be
akin to discarding 50 years of research in numerical approximation.

Best regards,

Guillaume