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
