This repository is a formalization, in Lean, of IEEE 754 decimal floating-point arithmetic. No, not binary floating-point arithmetic. Decimal arithmetic. Where "0.1" and "0.3" really are, exactly, 0.1 and 0.3, not a base-2 approximation thereof.
This work was motivated by the effort to add decimal numbers to JavaScript.
It is not necessary to do a formalization to shepherd a new language feature through the Ecma TC39 process. But the details of IEEE 754 can be a bit tricky. And because a feature that goes live in JavaScript essentially lives forever, and impacts a vast user base, it is critical to make sure that we're getting things just right.