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.
