# How can I prove facts about floating point calculations?

In computing, there is a standard called IEEE 754. Unlike in mathematics, computers have to fit numbers into a finite amount of space; to do this, they use a format a bit like scientific notation, called a double (or binary64, in later versions of the specification). It looks a little like this:

$$(-1)^a \times \left(1 + \frac{c}{2^{52}}\right) \times 2^{b-1023}$$

where $$a \in \{0,1\}$$; $$0\le b<2^{11}$$ and $$0\le c < 2^{52}$$.

$$a$$ is the sign, $$b$$ is the exponent and $$c$$ is the significand. It's a bit more complicated than that formula – there's a subnormal representation for numbers close to 0, so that 0 can be represented exactly – but there's not that much to it.

Integers are easy; you just consider all your arithmetic $$\mod {2^n}$$, and it's a finite field. Floating point arithmetic is harder; there's no guarantee that a + b - b equals a. All of the standard arithmetic operations on doubles have well-defined, exact values (for a given rounding mode), so it should be possible to prove things about floating point calculations, but I can't see how floats and doubles would map nicely to the sorts of elegant concepts that proof assistants use.

How do proof assistants represent floating point numbers, and how would I go about proving something like this?

$$a = 0.1 + 0.3 + 0.3 + 0.3 \\ b = 0.3 + 0.3 + 0.3 + 0.1 \\ a - b = 2^{-53}$$

• Ah, indeed, this is a more fundamental question than the one I asked about decimal floating points. Commented Feb 8, 2022 at 21:36
• @BrunoLeFloch I don't think either binary or decimal floating point is more fundamental than the other; they're both pretty far from the rationals and reals. I hadn't heard about Coq having support for this; do you happen to know any more about that? Commented Feb 8, 2022 at 21:41
• I just found coq-contribs/ieee754 from 1997 and "Flocq: A Unified Library for Proving Floating-Point Algorithms in Coq" from 2014 which states that they use their experience of earlier systems to make something better. Haven't looked yet, perhaps you'll beat me to it. Commented Feb 8, 2022 at 21:50
• According to another article it seems CompCert relies on Flocq to prove that floating point code in C is faithfully compiled. There is also a HOL proof for the exponential function. I can ask for some other pointers on the IEEE754 mailing list. Also a proof in the prover PVS. Commented Feb 8, 2022 at 21:53
• @BrunoLeFloch the Coq dev team missed a historical opportunity when Jesper Cockx became an Agda developer instead. Please consider contributing to the Flocq library. (I am already out. 🚪🚶) Commented Feb 23, 2022 at 9:22

I recommend the monograph Computer Arithmetic and Formal Proofs: Verifying Floating-point Algorithms with the Coq System by Sylvie Boldo and Guillaume Melquiond. It addresses your questions and much, much more.

You asked how proof assistants formalize floating points. The flocq library is a formalization of floating points in Coq. The Flocq in a Nutshell page explains how it works.

It is also possible to actually compute numerical approximations in a proof assistant, in a verified way. A prime example of how this is done is Formally Verified Approximations of Definite Integrals by Assia Mahboubi, Guillaume Melquiond, and Thomas Sibut-Pinote.

The HOL4 formalisations of floating point numbers define them as a record type:

float = <| Sign : word1; Exponent : 'w word; Significand : 't word |>


where the 'w and 't are polymorphic type variables allowing for words of different widths. 64-bit floats have 'w as 11, and 't as 52 (strictly, the types that have that many values). There are also functions defined to move back and forth between this representation and “unstructured” words that simply concatenate the bits of the various fields.

Arithmetic, NAN-ness and all the rest can then be defined on top of this foundation.