On Wednesday, 6 August 2014 at 17:19:45 UTC, Matthias Bentrup wrote:
> I still can't see how you can infer that the assume(!running)
> which clearly holds after the loop also holds before the loop.

It holds if the loop does not change running, trivially?
But then you no longer have a loop.

Note also that you can implement an if construct from while this way:

while(B){
S;
B=false;
}

If that was the case, then you could not infer anything about B before the while.

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?

The crux is the axiom that is being defined. When you write `assume(condition)`, the axiom is not:

    "`condition` is true."

but:

    "When control flow reaches this point, then `condition` is true."

It's not an unconditionally true condition :-P

On Wednesday, 6 August 2014 at 17:18:19 UTC, Sean Kelly wrote:
> So from a functional perspective, assuming this is a multithreaded app, what should the procedure be when an AssertError is thrown in some thread?

afaik, AssertError works the same as any other exception. If it reaches the top without being handled, then the entire app will be terminated including all the other threads.

On Wednesday, 6 August 2014 at 08:25:38 UTC, Walter Bright wrote:
> 4. everyone who wants faster assert optimizations will have to rewrite their (possibly extensive) use of asserts that we'd told them was best practice. I know I'd be unhappy about having to do such to my D code.

Also having the same syntax for both kinds of assert makes it easier to try unsafe optimizations: the code can be written safe, then unsafe optimizations can tried effortlessly and performance gains evaluated. In C one would only need to edit the macro to do this. Whether we want to allow such experiments is debatable, but I find it at least reasonable. One may also want the optimizations to propagate backwards for even more performance - this would be a different kind of optimization, which may or may not require yet another syntax.

On Wednesday, 6 August 2014 at 17:59:06 UTC, Marc Schütz wrote:
> The crux is the axiom that is being defined. When you write `assume(condition)`, the axiom is not:
>
>     "`condition` is true."
>
> but:
>
>     "When control flow reaches this point, then `condition` is true."
>
> It's not an unconditionally true condition :-P

Assume(X) does not provide a condition. It defines a proposition/relation to be true.

If you define a relation between two constants then it has to hold globally. Otherwise they are not constant…

Assume(P) defines that the proposition holds. If it does not involve variables, then it will be free to move anywhere by the rules of Hoare-logic (and propositional logic)? If assume(PI==3.14…) can move everywhere, by the rules, then so can assume(true==false).

You surely don't want to special case "true==false" in the hoare logic rules?

Please note that it is perfectly fine to define "true==false", but you then have to live by it, that is, you no longer have a boolean algebra, you have an unsound algebra.  And that holds globally. So, please don't think that assume(true==false) is a test of a condition, it is just a definition that you impose on the equality relation (that also, by incident, happens to make the algebra unsound)

If you special case assume(false) and assert(false) then you can no longer use deduction properly and it essentially becomes an aberration, syntactical sugar, that needs special casing everywhere.

It would be much better to just halt compilation if you at compile time can evaluate X==false for assume(X) or assert(X). Why let this buggy code live? If it failed at compile time then let the compilation fail! This would work better with CTFE.

"@unreachable" is an alternative if you want to be explicit about it and matches __builtin_unreachable et al.

On Wednesday, 6 August 2014 at 18:51:05 UTC, Ola Fosheim Grøstad wrote:
> On Wednesday, 6 August 2014 at 17:59:06 UTC, Marc Schütz wrote:
>> The crux is the axiom that is being defined. When you write `assume(condition)`, the axiom is not:
>>
>>    "`condition` is true."
>>
>> but:
>>
>>    "When control flow reaches this point, then `condition` is true."
>>
>> It's not an unconditionally true condition :-P
>
> Assume(X) does not provide a condition. It defines a proposition/relation to be true.

Well, let's call it proposition then...

>
> If you define a relation between two constants then it has to hold globally. Otherwise they are not constant…

Yes, but as I wrote above, we're not defining a relation between two constants ("true == false"), we define the following axiom:

    "When control flow reaches this point, then true == false."

Because true is not equal to false, it follows that the first part of the proposition cannot be true, meaning control flow will not reach this point.

>
> Assume(P) defines that the proposition holds. If it does not involve variables, then it will be free to move anywhere by the rules of Hoare-logic (and propositional logic)? If assume(PI==3.14…) can move everywhere, by the rules, then so can assume(true==false).

See above. Of course we could define our `assume(P)` to define `P` as an axiom directly, but this would be much less useful, because it would have exactly the consequences you write about. And it would be a lot more consistent, too. Surely you wouldn't want `assume(x == 42)` to mean "x is always and everywhere equal to 42", but just "x is equal to 42 when control flow passes this point".

>
> You surely don't want to special case "true==false" in the hoare logic rules?
>
> Please note that it is perfectly fine to define "true==false", but you then have to live by it, that is, you no longer have a boolean algebra, you have an unsound algebra.  And that holds globally. So, please don't think that assume(true==false) is a test of a condition, it is just a definition that you impose on the equality relation (that also, by incident, happens to make the algebra unsound)
>
> If you special case assume(false) and assert(false) then you can no longer use deduction properly and it essentially becomes an aberration, syntactical sugar, that needs special casing everywhere.
>
> It would be much better to just halt compilation if you at compile time can evaluate X==false for assume(X) or assert(X). Why let this buggy code live? If it failed at compile time then let the compilation fail! This would work better with CTFE.
>
> "@unreachable" is an alternative if you want to be explicit about it and matches __builtin_unreachable et al.

See above, no special treatment is necessary.

On Wednesday, 6 August 2014 at 19:18:30 UTC, Marc Schütz wrote:
>> Assume(P) defines that the proposition holds. If it does not involve variables, then it will be free to move anywhere by the rules of Hoare-logic (and propositional logic)? If assume(PI==3.14…) can move everywhere, by the rules, then so can assume(true==false).
>
> See above. Of course we could define our `assume(P)` to define `P` as an axiom directly, but this would be much less useful, because it would have exactly the consequences you write about. And it would be a lot more consistent, too. Surely you wouldn't want `assume(x == 42)` to mean "x is always and everywhere equal to 42", but just "x is equal to 42 when control flow passes this point".

This is unclear. What I wanted to write is: "It would be more consistent to use the definition of `assume` that I propose.".

On Wednesday, 6 August 2014 at 18:15:41 UTC, David Bregman wrote:
> On Wednesday, 6 August 2014 at 17:18:19 UTC, Sean Kelly wrote:
>> So from a functional perspective, assuming this is a multithreaded app, what should the procedure be when an AssertError is thrown in some thread?
>
> afaik, AssertError works the same as any other exception. If it reaches the top without being handled, then the entire app will be terminated including all the other threads.

Except that's not really how unhandled exceptions are treated in threads.  They're stored by the thread and (optionally) re-thrown in the context of whatever thread calls join, if any thread calls join at all.  The assumption at the time was that the joining thread cared about the state of the thread being joined and so re-throwing the exception was a way to communicate the error to the most interested party.

So if the main thread joins a thread that terminated with an unhandled AssertError, the error will be re-thrown in the context of the main thread, which will in turn join all remaining running threads and wait for them to complete.  This is the same behavior as if an AssertError is generated during normal processing of the main thread.  But in neither case is the application forcibly terminated when an assertion failure occurs.

So again, my question is twofold: what *should* happen, given this new treatment for assertions, and then *how* will we accomplish this?  A multithreaded process is really pretty much equivalent to a bunch of standalone processes with shared memory.  There is no facility for forcing a clean termination of another thread.  The best I can think of would be to assume that std.concurrency is being used for multithreading and sort things out similar to the existing LinkTerminated signaling, but looking for a reasonable solution within Druntime would be tricky.

On Wednesday, 6 August 2014 at 19:18:30 UTC, Marc Schütz wrote:
> On Wednesday, 6 August 2014 at 18:51:05 UTC, Ola Fosheim

> Yes, but as I wrote above, we're not defining a relation between two constants ("true == false"), we define the following axiom:
>
>     "When control flow reaches this point, then true == false."
>
> Because true is not equal to false, it follows that the first part of the proposition cannot be true, meaning control flow will not reach this point.

But you are defining an axiom, not evaluating, that is how the optimizer can use it for deduction. Think of how Prolog works.

> See above. Of course we could define our `assume(P)` to define `P` as an axiom directly, but this would be much less useful, because it would have exactly the consequences you write about. And it would be a lot more consistent, too. Surely you wouldn't want `assume(x == 42)` to mean "x is always and everywhere equal to 42", but just "x is equal to 42 when control flow passes this point".

I think there is a misunderstanding here. If you have:

uint x=0;

then that invokes many axioms defined by the language:

uint x=0;
assume(x exists from here)
assume(any value assigned to x has to be in the range [0,0xffffffff])
assume(x==0)
assume(type(x)=='uint')
assume(…etc…)

So if you then do:

x=x+1
assert(x==1)

You have to move the assert upwards (3+ steps) and see if it satisfied by any of the axioms you run into.

3: assert(x==0) //covered by axiom(x==0), x==1 is satisfied
2: assert(x+1-1==1-1)
1: assert(x+1==1)
x=x+1
assert(x==1)

Without the "uint x=0;" you would then have moved all the way up to the global scope (conceptually speaking) and not been able to find any axioms matching 'x'.

If you assume(x==0) on the other hand, then you don't need the other axioms at all. It is instantly satisfied. No need to prove anything.

> See above, no special treatment is necessary.

I don't follow. If you use assert(false) to signify anything special beyond requesting a proof or assume(false) for anything beyond defining an axiom, then you are special casing.

Please also remember that they are all "constants" in math, but variables are constants that are automatically renamed for convinience…

uint x=0;
x=x+1;
x=x*2;

is…

uint x0=0;
x1=x0+1;
x2=x1*2;

perhaps that makes it more clear.