On Wednesday, 27 January 2021 at 06:14:47 UTC, Ola Fosheim Grøstad wrote:
> On Wednesday, 27 January 2021 at 00:53:11 UTC, Bruce Carneal wrote:
>> You made an assertion, in a proof discussion, that the tractable extension of the exhaustive proof to cover larger FP types, was "no problem".
>
> Eh. I argued that you can fully cover an implementation without doing exhaustive testing. Don't confuse what I will waste my time on with what is possible.

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 that you later provided (those all enjoyed very clear domain co-domain mappings while suspected opacity of that mapping is the main concern regarding your "no problem" assertion).

Also, please understand that I do not regard your time as more 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.  Also note that "I was mistaken" and "I'm not sure what you mean, could you clarify x,y,z?" are perfectly acceptable responses (that I've used on more than one occasion and will, no doubt, use again in the future).

On Wednesday, 27 January 2021 at 08:27:13 UTC, Berni44 wrote:
> On Wednesday, 27 January 2021 at 01:16:40 UTC, Bruce Carneal wrote:
>> I'd vote for "overweight and almost-certainly-correct" over "trim but iffy" if the extra poundage is reasonable which, in the non-embedded environments, it appears to be.
>
> I'd like to compare the task to write floating point numbers to building a car: ...
>
>> A large body of others believe that ryu is a good way to go and are moving to standardize on it.
>>
>> It's not a live-or-die issue for me but ryu looks pretty good.
>
> We are in complete agreement here. My point is: Adding ryu printf would be the second step before the first step: First build ...

I'm quite confident that I have significantly less knowledge in this area than you do.  Your explanations/tutorials and corrections are welcome.  I'm just happy to see someone working on an important, foundational, capability.

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.

On Tue, Jan 26, 2021 at 11:16:58PM -0800, Walter Bright via Digitalmars-d wrote:
> On 1/26/2021 6:20 PM, Joseph Rushton Wakeling wrote:
> > On Wednesday, 27 January 2021 at 02:17:52 UTC, H. S. Teoh wrote:
> > > If there was a way to make these tables pay-as-you-go, I'd vote for it. Adding 104KB or 52KB even if the code never once formats a float, is not ideal, though granted, in this day and age of cheap, high-capacity RAM not really a big issue.
> > 
> > Agree completely -- pay-as-you-go should be important for something like this.  (But then, it should be important for the whole stdlib...)
> 
> I've always thought things like this should be in the operating system. Get it right once, then everyone uses it.

Or get it wrong once, and everyone rolls their own, all slightly wrong in a different way. :-D


> Date/time/DST should be in the OS, so should the ridiculously large amount of code to deal with the level 3 Unicode madness.

The next best thing is to reuse a reputable library that's reasonably widespread, like libicu.  But that adds an additional dependency, and the API isn't always conducive to how the language works.

Reuse is hard.


T

-- 
VI = Visual Irritation

On Wednesday, 27 January 2021 at 09:22:24 UTC, Bruce Carneal wrote:
> Your explanations/tutorials and corrections are welcome.

I added one more, going through the code in detail:

https://github.com/berni44/printFloat/blob/master/walkthrough.pdf

I hope this helps to tear down the fears somewhat...

On Wednesday, 27 January 2021 at 09:37:34 UTC, Ola Fosheim Grøstad wrote:
> On Wednesday, 27 January 2021 at 09:09:08 UTC, Bruce Carneal wrote:
>
> I haven't made any such assertion. If you ask questions, I'll answer them to my ability. Please stop making assumptions.

Great.  Two questions: 1) Do you believe that a trivial domain/co-domain mapping, like those in the examples you gave, exists for the problem under discussion? and 2) If so, do you have time to provide a proof?

On Wednesday, 27 January 2021 at 17:00:36 UTC, Bruce Carneal wrote:
> Great.  Two questions: 1) Do you believe that a trivial domain/co-domain mapping, like those in the examples you gave, exists for the problem under discussion? and

Certainly trivial from a theoretical perspective, in the sense that they are finite and therefore can be easily tabulated. If you want a more compact form you probably should look at modular arithmetics. You left out an important criterion, space-time efficiency.

The inverse mapping is also not terribly complex, but first you need to establish what you want to show. In the context of Phobos, minimal length is of little importance, it has not impact on correct usage. We don't have to care if the algorithm produces more digits than necessary, so we can limit ourselves to the inverse mapping from decimal to binary. Basically proving that we then get the x = f⁻¹(f(x)) = id(x).


> 2) If so, do you have time to provide a proof?

Proof of what? And are you willing to pay for it?

(I suggest you drop the juvenile tone, it is annoying.)

On Wednesday, 27 January 2021 at 22:49:11 UTC, Ola Fosheim Grøstad wrote:
> On Wednesday, 27 January 2021 at 17:00:36 UTC, Bruce Carneal wrote:
>> Great.  Two questions: 1) Do you believe that a trivial domain/co-domain mapping, like those in the examples you gave, exists for the problem under discussion? and
>
> Certainly trivial from a theoretical perspective, in the sense that they are finite and therefore can be easily tabulated. If you want a more compact form you probably should look at modular arithmetics. You left out an important criterion, space-time efficiency.
>
> The inverse mapping is also not terribly complex, but first you need to establish what you want to show. In the context of Phobos, minimal length is of little importance, it has not impact on correct usage. We don't have to care if the algorithm produces more digits than necessary, so we can limit ourselves to the inverse mapping from decimal to binary. Basically proving that we then get the x = f⁻¹(f(x)) = id(x).
>
>
>> 2) If so, do you have time to provide a proof?
>
> Proof of what? And are you willing to pay for it?
>
> (I suggest you drop the juvenile tone, it is annoying.

Perhaps you mistook my meaning when I used the term "trivial".  I could also have used "simple", "readily understood", "clearly provable", etc.

Regardless, you clearly do not understand what I'm asking in question 1) and I do not think it likely that additional interaction on this topic will be useful to either of us.

On 1/26/21 9:17 PM, H. S. Teoh wrote:
> 
> If there was a way to make these tables pay-as-you-go, I'd vote for it.
> Adding 104KB or 52KB even if the code never once formats a float, is not
> ideal, though granted, in this day and age of cheap, high-capacity RAM
> not really a big issue.

There is a way -- dynamic libraries. It's how C does it.

But seriously, I can't imagine why we are concerned about 100KB of code space. My vibe.d server is 80MB compiled (which I admit is a lot more than I would like, but still). My phone has as much code space as 100 computers from 10 years ago. Are you still using floppies to share D code?

-Steve

On Wed, Jan 27, 2021 at 10:18:58PM -0500, Steven Schveighoffer via Digitalmars-d wrote:
> On 1/26/21 9:17 PM, H. S. Teoh wrote:
> > 
> > If there was a way to make these tables pay-as-you-go, I'd vote for it.  Adding 104KB or 52KB even if the code never once formats a float, is not ideal, though granted, in this day and age of cheap, high-capacity RAM not really a big issue.
> 
> There is a way -- dynamic libraries. It's how C does it.

That's total overkill for 100KB of data.


> But seriously, I can't imagine why we are concerned about 100KB of code space. My vibe.d server is 80MB compiled (which I admit is a lot more than I would like, but still). My phone has as much code space as 100 computers from 10 years ago. Are you still using floppies to share D code?
[...]

It's not so much this specific 100KB that I'm concerned about; it's the general principle of pay-as-you-go.  You can have 100KB here and 50KB there and 70KB for something else, and pretty soon it adds up to something not so small. Individually they're not worth bothering with; together they can add quite a bit of bloat, which may be desirable to get rid of, for embedded applications say.


T

-- 
What doesn't kill me makes me stranger.