August 03, 2014
On Saturday, 2 August 2014 at 17:36:46 UTC, David Bregman wrote:
> OK, I'm done. It's clear now that you're just being intellectually dishonest in order to "win" what amounts to a trivial argument. So much for professionalism.

Haha, this time it's not as bad as it was in catch syntax discussion. I even thought then they are blackmailed or something like that.
August 04, 2014
On 8/3/14, 11:55 AM, Kagamin wrote:
> On Saturday, 2 August 2014 at 17:36:46 UTC, David Bregman wrote:
>> OK, I'm done. It's clear now that you're just being intellectually
>>  dishonest in order to "win" what amounts to a trivial argument. So
>>  much for professionalism.
>
> Haha, this time it's not as bad as it was in catch syntax discussion.
> I even thought then they are blackmailed or something like that.

It's really only this kind of stuff that has Walter and myself worried.
We understand spirits can get heated during a debate but the problem
with such comebacks that really hold no punches is they instantly
degrade the level of conversation, invite answers in kind, and are very
difficult to respond to in meaningful ways.

From what I can tell after many years of having at this, there's a sort
of a heat death of debate in which questions are asked in a definitive,
magisterial manner (bearing an odd implied binding social contract), and
any response except the desired one is instantly dismissed as simply
stupid, intellectually dishonest, or, as it were, coming under duress.

I can totally relate to people who hold a conviction strong enough to
have difficulty acknowledging a contrary belief as even remotely
reasonable, as I've fallen for that many times and I certainly will in
the future. Improving awareness of it only improves the standing of
debate for everyone involved.

For my money, consider Walter's response:

> What I see is Microsoft attempting to bring D's assert semantics into
> C++. :)
>
> As I've mentioned before, there is inexorable pressure for this to
> happen, and it will happen.

I find it to the point, clear, and funny. Expanded it would go like "I see more similarities than differences, and a definite convergence dictated by market pressure." I find it highly inappropriate to qualify that response as intellectually dishonest even after discounting for a variety of factors, and an apology would be in order.


Andrei
August 04, 2014
On Monday, 4 August 2014 at 00:59:10 UTC, Andrei Alexandrescu wrote:
> On 8/3/14, 11:55 AM, Kagamin wrote:
>> On Saturday, 2 August 2014 at 17:36:46 UTC, David Bregman wrote:
>>> OK, I'm done. It's clear now that you're just being intellectually
>>> dishonest in order to "win" what amounts to a trivial argument. So
>>> much for professionalism.
>>
>> Haha, this time it's not as bad as it was in catch syntax discussion.
>> I even thought then they are blackmailed or something like that.
>
> It's really only this kind of stuff that has Walter and myself worried.
> We understand spirits can get heated during a debate but the problem
> with such comebacks that really hold no punches is they instantly
> degrade the level of conversation, invite answers in kind, and are very
> difficult to respond to in meaningful ways.
>
> From what I can tell after many years of having at this, there's a sort
> of a heat death of debate in which questions are asked in a definitive,
> magisterial manner (bearing an odd implied binding social contract), and
> any response except the desired one is instantly dismissed as simply
> stupid, intellectually dishonest, or, as it were, coming under duress.
>
> I can totally relate to people who hold a conviction strong enough to
> have difficulty acknowledging a contrary belief as even remotely
> reasonable, as I've fallen for that many times and I certainly will in
> the future. Improving awareness of it only improves the standing of
> debate for everyone involved.
>
> For my money, consider Walter's response:
>
>> What I see is Microsoft attempting to bring D's assert semantics into
>> C++. :)
>>
>> As I've mentioned before, there is inexorable pressure for this to
>> happen, and it will happen.
>
> I find it to the point, clear, and funny. Expanded it would go like "I see more similarities than differences, and a definite convergence dictated by market pressure." I find it highly inappropriate to qualify that response as intellectually dishonest even after discounting for a variety of factors, and an apology would be in order.

It's easy to get a very different impression from his post: "I don't want to counter your arguments, so I just pick a random snippet from your post and make a funny mostly irrelevant comment, while ignoring everything else you wrote."

Now, I don't believe that this was Walter's intention, but in the end it had the same effect :-( This is very bad, because I feel this discussion is important, so it matters for both sides to understand where the others are coming from. We can't achieve this by evading questions and discussion. And it wasn't just this one post; if you look at the discussion, there are entire sub-threads where people were obviously just talking past each other. But for me it's not easy to see _why_ they were doing it, i.e. what exactly the misunderstanding is.
August 04, 2014
On Monday, 4 August 2014 at 00:59:10 UTC, Andrei Alexandrescu
wrote:
> I find it to the point, clear, and funny. Expanded it would go like "I see more similarities than differences, and a definite convergence dictated by market pressure."

I find this to be a non-sequitur. Firstly, making a joke to avoid
answering a direct question is hardly what I'd call "to the
point", regardless of how funny it may be. Secondly, even if I
interpreted it as you did, it still misses the point. The
discussion was about strict logical semantic equivalence of two
concepts, assert and assume. How can "I see more similarities
than differences, and a definite convergence dictated by market
pressure" be a response to a black and white question about
semantic equivalence?

> I find it highly inappropriate to qualify that response as intellectually dishonest even after discounting for a variety of factors, and an apology would be in order.

Sure, that post alone isn't sufficient, but Walter argued much of
the discussion in an unfair manner: dismissive one liners,
fallacious arguments, strawman, even straight up begging the
question. We are talking about several dozens of posts here.
There was more than enough time spent to converge on agreement,
if both sides intended to do so. Anyways I know this is all
completely pointless to say, no one is going to believe it
for one second because it just sounds like poor sportsmanship.
For anyone who actually cares, you just need to read the threads
and judge for yourself. From where I stand though, no apology is
required.
August 05, 2014
On Monday, 4 August 2014 at 00:59:10 UTC, Andrei Alexandrescu wrote:
> For my money, consider Walter's response:
>
>> What I see is Microsoft attempting to bring D's assert semantics into
>> C++. :)
>>
>> As I've mentioned before, there is inexorable pressure for this to
>> happen, and it will happen.
>
> I find it to the point, clear, and funny.

Yeah, it was funny because:
( http://msdn.microsoft.com/en-us/library/1b3fsfxw.aspx )

«Caution:
A program must not contain an invalid __assume statement on a reachable path. If the compiler can reach an invalid __assume statement, the program might cause unpredictable and potentially dangerous behavior.»

Please note «if the compiler can reach», not «if a path can be executed».


And «inexorable»:
( https://www.google.no/search?q=inexorable )

- "the seemingly inexorable march of new technology"

- (of a person) impossible to persuade; unrelenting.


Of course, being unrelenting goes with the territory of single-handedly building a c++ competitor. So it is not a bad trait. The bad thing here is not making "compile assert as assume" an experimental feature, but making it the default.

People who are autodidact also sometimes find new ways of doing things because they are more likely to go explore new paths. But I don't think this path is all that new… so I hope Walter, if he continues walking down this path, remains unrelenting and keeps walking past "assert as assume" until he finds truly new territory in the realm of formal methods. That could happen and bring great features to D.

There is a significant difference between going down a path to see what you can find on the other end and turning the path into a goal, a priori.
August 05, 2014
On Tuesday, 5 August 2014 at 09:42:26 UTC, Ola Fosheim Grøstad wrote:
> On Monday, 4 August 2014 at 00:59:10 UTC, Andrei Alexandrescu wrote:
>> For my money, consider Walter's response:

I feel a bit confused about the mixture between compiler and optimizer. While I agree the compiler does the optimization and the two are intrinsically linked, the languages (or the instructions) for them seem to me to belong to quite different paradigms:

- compiler language is imperative programming
- optimizer language is declarative programming

It is wise to mix them to such degree as to no longer distinguish them? For me, assume and the like shall rather go with the annotations.
August 05, 2014
On Tuesday, 5 August 2014 at 10:00:55 UTC, eles wrote:
> It is wise to mix them to such degree as to no longer distinguish them? For me, assume and the like shall rather go with the annotations.

That's one of the reasons I think it is not new territory, since letting assert have side effects basically sounds like constraints programming/logic programming.

I do think that constraints programming has a place in support for generic programming and other things that can be known to evaluate at compile time. So I think imperative programming languages are going to become hybrids over time.

Also, if you think about the new field "program synthesis", where you specify the constraints to generate/fill out boiler code in an imperative program, then the distinction becomes blurry. Rather than saying sort(x) you just specify that the outcome should be sorted in the post condition, but don't care why it ended up that way. So the compiler will automatically add sort(x) if needed. Sounds like a powerful way to get rid of boring programming parts.

Another point, when you think about it, Program Verification and Optimization are conceptually closely related.

S = specification // asserts is a weak version of this
P = program
E = executable

ProgramVerification:
Prove( S(x)==P(x) for all x )

Optimization Invariant:
Prove( P(x)==E(x) for all x )
August 05, 2014
On Monday, 4 August 2014 at 00:59:10 UTC, Andrei Alexandrescu wrote:
> I can totally relate to people who hold a conviction strong enough to
> have difficulty acknowledging a contrary belief as even remotely
> reasonable

Yes, it's difficult to acknowledge a belief, reason for which wasn't provided, but instead "we have nothing to add" reply was given.
August 05, 2014
On Tuesday, 5 August 2014 at 09:42:26 UTC, Ola Fosheim Grøstad wrote:
> But I don't think this path is all that new… so I hope Walter, if he continues walking down this path, remains unrelenting and keeps walking past "assert as assume" until he finds truly new territory in the realm of formal methods. That could happen and bring great features to D.

This! +1000!

This is what I've been feeling too: Walter is wrong - astonishingly wrong in fact - but in a very interesting direction that may have something very 'right' on the other side of it. I don't know what form it will take, but the example
someone gave, of keeping track of when a range is sorted vs. not known to be sorted, to me gives a hint of where this may lead. I can't quite imagine that particular example playing out, but in general if the compiler keeps track of properties of things then it could start making algorithmic-level performance decisions that today we always have to make by hand. To me that's interesting.

August 06, 2014
On Tuesday, 5 August 2014 at 16:35:42 UTC, Andrew Godfrey wrote:
> out, but in general if the compiler keeps track of properties of things then it could start making algorithmic-level performance decisions that today we always have to make by hand. To me that's interesting.

I think the most "potent" source for optimization is getting expressive formalisms in place for allowing axioms and theorems to pass through foreign function calls.

That would allow you to call custom C functions/machine language in  a loop with less penalties.