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.
