Printing floating points

[Ola Fosheim Grøstad]

On Friday, 29 January 2021 at 18:35:54 UTC, Ola Fosheim Grøstad 
wrote:
> On Friday, 29 January 2021 at 14:24:17 UTC, Bruce Carneal wrote:
>> Then I misunderstood you all along.  I thought that you were 
>> describing something that would be part of a formal proof.
>
> A formal proof would have to be machine checked. So you need a 
> good solver/verifiers. And experience to make good use of, and 
> patience... I think we can safely say that this is out of scope 
> for the D community at this point.

And you would also need to annotate the D code with Hoare logic 
and generate verification conditions. Although there are tools 
that can help with that. But you would still need expertise to 
make good use of it. It is not a push-button topic.

The only other alternative would be bit blasting, as I mentioned, 
which may or may not work out. Probably not if the code is too 
convoluted, but it might. Depends on the solver and structure of 
the input.