The Coq mailing list

[Laurent Théry <Laurent.Thery AT inria.fr>]

On 05/07/15 01:11, Eric Mullen wrote:
> There's Flocq, which is used by CompCert to formalize floating point:
> http://flocq.gforge.inria.fr/

Flocq floats are executable inside Coq but I am not sure it extracts
to something more efficient outside Coq.

> As for relating it to rationals, that will be tough. Rational arithmetic is
> quite fundamentally different than floating point: e.g. addition commutes
> in the rationals, but doesn't in the floats.
I think it is more associativity that is a problem.

> > It would be awesome if this interface also includes a logical
> > specification of the floating point operations, perhaps in terms of Coq
> > rationals (Coq.QArith.QArith_base.Q).

Proving anything about floats, you often need to know exactly which kind 
of floats you are manipulating (precision, format, round modes).
So it makes sense to stick to the IEEE754 standard. I am not sure 
Haskell is compliant with it.

--
Laurent