Printing floating points

[John Colvin]

On Tuesday, 26 January 2021 at 19:02:53 UTC, Bruce Carneal wrote:
> 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?

You can probably inductively prove - or at least become quite 
certain - that your implementation is identical to the original 
algorithm within a given set of inputs, given one good result 
within that set. What those sets look like depends on the 
algorithm of course.

E.g. given an algorithm for a function with type integer -> 
integer, if you can prove your implementation of an algorithm is 
linear w.r.t. its input and you can demonstrate it's correct for 
1, you can then infer it will be correct for any other integer 
input. I think? Off the top of my head.

Of course <insert interesting algorithm here> isn't linear w.r.t. 
its inputs, but maybe it is within some fixed subset of its 
inputs, so you only have to test one of those to cover the whole 
set. Also, linearity isn't the only property one can consider.