On Wednesday, 6 August 2014 at 15:29:13 UTC, Ola Fosheim Grøstad
wrote:
> On Wednesday, 6 August 2014 at 15:02:10 UTC, Matthias Bentrup wrote:
>> is equivalent to
>>
>>  while(running) {
>>    ...don't assign to running, don't break...
>>  }
>>  assume(!running);
>
> You have to prove termination to get there? Plain Hoare logic cannot deal with non-terminating loops. Otherwise you risk proving any theorem below the loop to hold?
>

I'm pretty sure that running is false when the program reaches
the end of the while loop, whether it is assigned in the loop or
not. I only added the "don't assign to running" to make the
example match your pattern.

On Wednesday, 6 August 2014 at 00:50:07 UTC, Walter Bright wrote:
> On 8/3/2014 4:24 PM, Martin Krejcirik wrote:
>> Couldn't this new assert behaviour be introduced as a new optimization
>> switch ? Say -Oassert ? It would be off by default and would work both
>> in debug and release mode.
>
> It could, but every one of these:
>
> 1. doubles the time it takes to test dmd, it doesn't take many of these to render dmd untestable
>
> 2. adds confusion to most programmers as to what switch does what
>
> 3. adds complexity, i.e. bugs

If performance is not worth associated complexity, then it doesn't pull its weight.

> 4. interactions between optimization switches often exhibits emergent behavior - i.e. extremely hard to test for

Why do you think the emergent behavior is caused by interactions between switches, you think optimizations themselves don't interact? You said, it's factorial, is it a number of permutations of switches or a number of permutations of optimizations? Switches should not be sensitive to permutations.

On Wednesday, 6 August 2014 at 08:25:38 UTC, Walter Bright wrote:
> 1. it's long with an unappealing hackish look

It's an established practice in D that unsafe features should look unappealing. Example: __gshared.

> 3. users will be faced with two kinds of asserts, with a subtle difference that is hard to explain, hard to remember which is which, and will most likely use inappropriately

Andrei already proposed `debug assert` - a safe flavor of (dangerous by default) assert. So two kinds of assert are inevitable and should be documented, because user should be informed about dangerous optimizations. But frankly "compiler will break your code" is not a subtle difference and can be easily explained in just 5 words.

And BTW why safe behavior must be invoked with an extra syntax? That goes against best D practices and hence surprising, confusing and counterintuitive.

> I'll sum up with the old saw that any programming problem can be solved with another level of indirection. I submit a corollary that any language issue can be solved by adding another keyword or compiler flag. The (much) harder thing is to solve a problem with an elegant solution that does not involve new keywords/flags, and fits in naturally.

So what is this elegant solution? To break code silently in the worst possible way and selectively and exactly at the most critical points?

Another downside of assert being dangerous - you can't add it to code freely. Every assert can order the compiler to break the code, adding an assert becomes a difficult task, because the asserted expression (being assumed) begins to require a thorough future-proof environment-independent proof, which is very hard to come by: it needs to be an actual proof than just a guess, because the tradeoff is to be literally punished by death. Unittests don't provide such proof.

On Wednesday, 6 August 2014 at 16:42:57 UTC, Matthias Bentrup wrote:
> I'm pretty sure that running is false when the program reaches
> the end of the while loop, whether it is assigned in the loop or
> not. I only added the "don't assign to running" to make the
> example match your pattern.

Well, if you don't assign to it in the loop, and it is known to terminate, then "running" is provably false before the loop for sure?

But then it isn't a loop… It is an empty statement: skip, NOP…

On 08/06/14 18:00, via Digitalmars-d wrote:
> I am quite confident that assume(false) anywhere in your program is basically stating that the program is unsound (true==false) and should not be compiled and run at all.

No, an assume(false) in a program only means that every _path_
_leading_to_that_statement is 'unsound'. For practical purposes
it's better to treat 'unsound' as impossible and unreachable.

IOW

    import std.stdio, std.array;
    int main(string[] argv) {
       if (argv.length<2)
          assume(0);
       if (argv.length==1)
          writeln("help text");
       return argv.empty;
    }

=>

0000000000403890 <_Dmain>:
   403890:       31 c0                   xor    %eax,%eax
   403892:       c3                      retq


The alternatives would be to make it either: a) always a compile
error, or b) always a runtime error. The former would add little
value (`static assert` already exists); the latter is already
available as `assert(0)`.
The above example after "s/assume(0)/assert(0)/" becomes:

0000000000403890 <_Dmain>:
   403890:       48 83 ff 01             cmp    $0x1,%rdi
   403894:       76 03                   jbe    403899 <_Dmain+0x9>
   403896:       31 c0                   xor    %eax,%eax
   403898:       c3                      retq
   403899:       50                      push   %rax
   40389a:       e8 71 e7 ff ff          callq  402010 <abort@plt>

IOW the compiler can still optimize based on the (un)reachability,
but the behavior in no longer undefined.

artur

On Wednesday, 6 August 2014 at 16:00:33 UTC, Ola Fosheim Grøstad wrote:
> On Wednesday, 6 August 2014 at 15:36:52 UTC, Marc Schütz wrote:
>> This is an assume, not an assert.
>
> Not sure what you mean. An assume is an assert proven (or defined) to hold. It can be a proven theorem which has been given the status of an axiom. It is known to keep the algebraic system sound. If you claim that something unsound is proven then all bets are off everywhere?

I guess we're talking past each other. You were saying that Hoare logic doesn't work with non-terminating loops, and I was responding that there was no non-terminating loop in the example. That's all there is to it.

To clarify: The assume condition wasn't `false`, it was `!running`. There is a situation in which this is true, namely when `running` is false at the point where the assume is. Because the variable isn't changed in the loop, it follows that it's also true before the loop. I see no contradiction here.

On Wednesday, 6 August 2014 at 16:59:18 UTC, Artur Skawina wrote:
> No, an assume(false) in a program only means that every _path_
> _leading_to_that_statement is 'unsound'. For practical purposes
> it's better to treat 'unsound' as impossible and unreachable.

I don't think so. Because a program is only correct if all axioms and proposed theorems are proven true.

All axioms are by definition true, so if you assume(false==true) anywhere it has to hold everywhere. Neither "false" or "true" are variables.

Just like assume(PI==3.14…) has to hold everywhere. false, true and PI are constant throughout every path in the program.

Not really sure how it is possible to disagree with that?

On Wednesday, 6 August 2014 at 17:03:44 UTC, Marc Schütz wrote:
> I guess we're talking past each other. You were saying that Hoare logic doesn't work with non-terminating loops, and I was responding that there was no non-terminating loop in the example. That's all there is to it.

Oh well, but a terminating loop that does not change the condition is just an empty statement. So then you have basically proved that it isn't a loop… ;)

So from a functional perspective, assuming this is a multithreaded app, what should the procedure be when an AssertError is thrown in some thread?

On Wednesday, 6 August 2014 at 17:08:18 UTC, Ola Fosheim Grøstad
wrote:
> On Wednesday, 6 August 2014 at 17:03:44 UTC, Marc Schütz wrote:
>> I guess we're talking past each other. You were saying that Hoare logic doesn't work with non-terminating loops, and I was responding that there was no non-terminating loop in the example. That's all there is to it.
>
> Oh well, but a terminating loop that does not change the condition is just an empty statement. So then you have basically proved that it isn't a loop… ;)

I still can't see how you can infer that the assume(!running)
which clearly holds after the loop also holds before the loop.

On Wednesday, 6 August 2014 at 17:03:45 UTC, Ola Fosheim Grøstad wrote:
> On Wednesday, 6 August 2014 at 16:59:18 UTC, Artur Skawina wrote:
>> No, an assume(false) in a program only means that every _path_
>> _leading_to_that_statement is 'unsound'. For practical purposes
>> it's better to treat 'unsound' as impossible and unreachable.
>
> I don't think so. Because a program is only correct if all axioms and proposed theorems are proven true.
>
> All axioms are by definition true, so if you assume(false==true) anywhere it has to hold everywhere. Neither "false" or "true" are variables.
>
> Just like assume(PI==3.14…) has to hold everywhere. false, true and PI are constant throughout every path in the program.
>
> Not really sure how it is possible to disagree with that?

These threads have proven that it's apparently possible to disagree
even about the definition of words like "disagreement" and
"definition"...

But, in a practical programming language definition context,
consider:

   if (0)
      assume(0);

Yes, `assume` could be defined in a way that would make this
always a compile error. But then `assume(0)` would be useless.
If it means 'unreachable' instead, then the behavior is still
consistent - it becomes a way to to tell the compiler: "this
can never happen, optimize accordingly".

[gmail smtp servers seem to be broken right now; had to post this
 via the webform; probably won't be posting until the mailing list
 i/f starts working for me again]

artur