The Coq mailing list

[Andrej Bauer <andrej.bauer AT andrej.com>]

MPFR is *not* an implementation of real numbers. One run of mpfr
corresponds roughly to one iteration of iRRAM computation. MPFR is not
able to adapt precision automatically.

Anyhow, it is *very* easy to get an implementation of real numbers
wrong without having a clear theoretical model. An implementation of
reals is not an implementation until it implements the essential
structure of reals, which are the field operations and completeness
(either Cauchy or Dedekind).

With kind regards,

Andrej


On Sat, Jun 23, 2012 at 10:21 PM, Freek Wiedijk 
<freek AT cs.ru.nl>
 wrote:
> Hi Andrej,
>
>>>>and quite likely the fastest one around,
>
>>I'll count Mathematica in when they tell me how it works.
>
> :-)  I was just reacting to the "fastest one".  I was
> surprised as well that they were faster than the dedicated
> systems.  But they clearly were.
>
> As you can see from the paper, mpfr was also faster than
> iRRAM.  At least back then.
>
> Freek