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?
