Printing floating points

[Ola Fosheim Grøstad]

On Wednesday, 27 January 2021 at 09:09:08 UTC, Bruce Carneal 
wrote:
> No, you made an assertion regarding the tractable extension of 
> an exhaustive proof from 32 bits to longer FP representations 
> for a particular implementation, a problem that I believe to be 
> wholly unlike the simple examples

The original statement was that there was only a choice between 
exhaustive testing and a full formal proof. Then there was 
confusion between proving the correctness of tables, algorithms 
and the actual implementation.

Nobody wants to implement an algorithm for which there are no 
proofs of correctness. That is the basic foundation we have to 
presume, so a proof of the  abstract algorithm is not wasted even 
if you only test the implementation. That proof is kinda part of 
the specification you base your implementation and testing on.

When you implement the algorithm you also have to consider how it 
will be tested (including partial proofs). The "no problem" as 
related to not having to choose between an exhaustive proof and 
full formal verification. Neither option is likely in the D 
community.

I pointed out that one can test the boundary cases. I have 
clearly not studied the details of the implementation. It was a 
general suggestion for when neither a full formal proof is likely 
or exhaustive testing is reasonable.


> valuable than the time of your readers.  In that spirit I 
> suggest that direct answers to questions regarding simple 
> topics ("no problem" topics), are preferable to assertions that 
> you don't have time to help others understand.

I haven't made any such assertion. If you ask questions, I'll 
answer them to my ability. Please stop making assumptions.

We are talking about finite input, finite input, small scale, and 
fairly regular. Clearly not intractable.