Printing floating points

[Bruce Carneal]

On Tuesday, 26 January 2021 at 20:27:25 UTC, Ola Fosheim Grøstad 
wrote:
> On Tuesday, 26 January 2021 at 19:02:53 UTC, Bruce Carneal 
> wrote:
>> 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.
>
> Of course you do, you need proof of the tests being correct...

I believed that to be obvious.  There is no utility in 
exhaustively looping over tests that are incorrect.  The domain 
<==> co-domain properties in this case means that the correctness 
check is direct.

>
>> can be skipped is tantamount to saying that you know the 
>> implementation performs correctly in those regions.
>
> In general, if one understands the algorithm as implemented 
> then one can either manually or automatically prove certain 
> regions/ranges. Then you only need to test the regions/ranges 
> that are hard to prove.
>
> For instance, for a converter from int to string, the most 
> likely failure point will be tied to crossing between "9" and 
> "0" as well as the ends of the base-2 input. Meaning, if it 
> works for 1,2,3, you know that it also works for 4,5,6,7,8, but 
> maybe not 9,10.

Yes.  So now we have to prove that we can subset the exhaustive 
test.

This is something like the algorithm development technique that 
starts with a backtracking solution (full enumeration) and then 
prunes away via memoization or other to achieve a lower 
complexity.  If, OTOH, I start in the middle, asserting that I 
"know" what the shape of the problem is, then I'm on shaky ground.

As practicing programmers we live with "shaky ground" every day, 
but I'm hoping we can do better in this case.  It's already 
moving in a good direction.