Printing floating points

[Bruce Carneal]

On Thursday, 28 January 2021 at 23:27:28 UTC, Ola Fosheim Grøstad 
wrote:
> On Thursday, 28 January 2021 at 15:13:57 UTC, Bruce Carneal 
> wrote:
>> For the problem under discussion the domain is 0 .. 2**NBits 
>> (binary FP) and the codomain is the problem specified string 
>> output of the function.  This has not changed and I had 
>> thought it was clear to all concerned throughout.
>
> Let's backtrack then. My suggestion was that one does an 
> informal proof of the easier aspects one can reason about and 
> then do testing to cover those aspects which one cannot 
> convince oneself of. So in order to list those tests one would 
> have to do a deep analysis of the actual implementation 
> informed by the properties/proofs of the abstract algorithm 
> (the spec). Without such an analysis one cannot give examples 
> of dependencies expressed as propositions.
>
> The core problem float2string is comparable to 
> fixedpoint2string which is comparable to integer2string, 
> because the transform from float to fixed point is trivial. (We 
> also note that float is base2 and the target is base10, and 
> that 10=5·2 so we may be rewarded for paying attention to 
> modulo 5.) Then we may choose to represent a base 10 digit with 
> something that is easier to deal with for a solver. We then 
> need to think about, not increments of 1, but relationships in 
> terms of modular arithmetic/congruence - related formalizations.
>
>
>> I am actually interested in proving correctness by 
>> establishing full coverage of the domain with something less 
>> expensive than direct enumeration, less expensive than a for 
>> loop across all possibilities (an SMT-like solution).
>
> SMT/SAT based solutions are not like a for-loop across all 
> possibilities.

No, of course not.  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.

>
> Are you actually serious about proving correctness? I don't get 
> that feeling.
>
>
>> You have no particular insight to offer toward the solution of 
>> the above problem and, by your lights, never made such a claim.
>
> I am not sure what you mean by this, but you sure manage to 
> make it sound offensive... I've suggested utilizing 
> bit-blasting, identity transform, modular arithmetics etc. I've 
> never hinted or suggested that I have any intent of working on 
> this problem, and explicitly stated that I have not taken a 
> close look at the Mir implementation, nor do I intend to.
>
> I do however refute the idea that an exhaustive test is needed, 
> since the problem involves regular patterns.

Well, you've not refuted anything that I can see.  You've 
asserted something, yes, something that I think is quite useful 
if provable.  The intutition that prompts you to make such an 
assertion is what I'm most interested in.  I do not believe the 
assertion is provable but would be very happy to be proven wrong 
as that would be a win for everyone.

Since you continue to take offense at my writing, where none was 
intended, I think direct two way communication would be better 
than continuing here.  I'll be hanging out at beerconf if you 
think it's worth your time to converge on understanding.  Even if 
we aren't able to take your intuition to a proof or refutation 
quickly, we should at least be able to comprehend a lack of ill 
will.