Printing floating points

[Bruce Carneal]

On Tuesday, 26 January 2021 at 19:47:47 UTC, John Colvin wrote:
> 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.

Yes.  If we can define, with confidence, a representative set 
which spans the entire domain then we're good to go: inductive, 
piecewise, whatever.  We trade one proof (the original) for 
another (that the coverage is exhaustive/sufficient).  That can 
be a great trade but I'm not confident in my ability to define 
such a set in this case (gt 32 bit floats).  Perhaps others are 
confident.

However it goes from this point on, I'm very happy to see the 
progress made towards repeatability, towards solid foundations. 
My thanks to those hammering on this for the rest of us.