assert semantic change proposal

via Digitalmars-d digitalmars-d at puremagic.com
Wed Aug 6 10:59:04 PDT 2014


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


More information about the Digitalmars-d mailing list