assert semantic change proposal

[via Digitalmars-d]

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.