Remix.run Logo
nrr 3 hours ago

> I implemented float-to-string for my compiler's printf back sometime before 1985. It's a medium difficult problem.

It might have been medium difficult back in 1985, but the state of the art has progressed in the intervening 40 years. The constraint of correctness makes things trickier because it further imposes three requirements: completeness, uniqueness, and determinism.

Unless the implementer has the skill to prove these properties about the algorithm they've implemented, such an implementation is likely not to achieve those requirements.

WalterBright 2 hours ago | parent [-]

There was no test suite for it available that I could use for correctness checks, so I did what I could.

I also implemented IEEE 754 floating point in asm. For that I did have an exhaustive test suite, and passed it 100%.

nrr 23 minutes ago | parent [-]

We didn't have this definition of correctness until 1990 (due to Steele and White), and it wasn't until the past decade or so that we got a published algorithm (most recently, I think, Dragonbox, due to Jeon when he was still working on his PhD at UCSD), with mathematical proof[0], that satisfied all of the requirements of being complete, being unique, and being deterministic.

(Though, Steele-White expresses these slightly differently, as preserving information, having the shortest possible output, and rounding correctly. Completeness, uniqueness, and determinism seem to be equivalent and are easier to prove.)

--

0: Available at <https://fmt.dev/papers/Dragonbox.pdf>. It's pretty easy to understand either with a numerical analysis background or after having worked through volume 2 of Knuth's TAoCP.