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?
These threads have proven that it's apparently possible to
disagree
even about the definition of words like "disagreement" and
"definition"...
But, in a practical programming language definition context,
consider:
if (0)
assume(0);
Yes, `assume` could be defined in a way that would make this
always a compile error. But then `assume(0)` would be useless.
If it means 'unreachable' instead, then the behavior is still
consistent - it becomes a way to to tell the compiler: "this
can never happen, optimize accordingly".
[gmail smtp servers seem to be broken right now; had to post this
via the webform; probably won't be posting until the mailing list
i/f starts working for me again]
artur
