Printing floating points

[Bruce Carneal]

On Friday, 29 January 2021 at 13:42:49 UTC, Ola Fosheim Grøstad 
wrote:
> On Friday, 29 January 2021 at 02:58:38 UTC, Bruce Carneal wrote:
>> The parenthetical phrase was meant to apply to everything that 
>> preceeded it.  An SMT like solution is what I thought you had 
>> asserted, something that substantially cut down the work while 
>> provably covering the full domain.
>
> I am not asserting anything, other than that I don't think full 
> formal verification (unless bitblasting works) is within the 
> perimeter of the D community, so that leaves informal proofs 
> combined with selective testing as the viable option that the D 
> community as a whole (not any specific individual) can 
> accomplish.

Then I misunderstood you all along.  I thought that you were 
describing something that would be part of a formal proof.

As an aside: I consider an exhaustive f32 proof to be very strong 
evidence that an implementation will likely be correct for larger 
formats.

>
> A solver is a tool that can be used to make this viable. 
> Without a solver, maybe a reimplementation with a 
> correspondence proof is easier.
>
>
>> better than continuing here.  I'll be hanging out at beerconf 
>> if you think it's worth your time to converge on understanding.
>
>
> I like the idea of beerconf, but I have a deliverable deadline 
> on monday, so I don't have time this week.

OK.  I hope we have the opportunity to chat directly at a later 
date.  Good luck meeting your deadline.