On the other hand, they (unexpectedly to the inventor, who intended them to be a debugging tool) underpin a few foundational results in correctly rounded computation, such as https://en.wikipedia.org/wiki/Sterbenz_lemma.

> Even their inventor had trouble writing correct code in their presence

I didn't know that. Could you provide a more specific reference?