Printing floating points

[Bruce Carneal]

On Tuesday, 26 January 2021 at 16:31:35 UTC, Ola Fosheim Grøstad 
wrote:
> On Monday, 25 January 2021 at 21:40:01 UTC, Bruce Carneal wrote:
>> If I'm wrong, if it really is as you say "no problem", then 
>> the RYU author sure wasted a lot of time on the proof in his 
>> PLDI 2018 paper.
>
> Why is that? If the proof is for the algorithm then it has 
> nothing to do with proving your implementation to be correct.

If you can construct a tractable exhaustive proof of an 
implementation, which is what I believe you asserted in this 
case, then you don't need any other proof.

I'm very happy to see the 32 bit floats done exhaustively BTW.  
It is very suggestive, but not definitive if I understand the 
problem correctly.

The mapping from the domain to the co-domain is the entire 
problem IIUC so asserting that certain ranges within the domain 
can be skipped is tantamount to saying that you know the 
implementation performs correctly in those regions.  What am I 
missing?