assert semantic change proposal

[via Digitalmars-d]

On Thursday, 7 August 2014 at 08:12:23 UTC, Matthias Bentrup 
wrote:
> So the D function (note that "a" is constant)
>
> int silly() {
>   enum int a = 1;
>   if( a == 2 ) {
>     assert( a == 2 );
>   }
>   return a;
> }
>
> has undefined semantics (at least in debug mode), because it 
> contains a false assertion ?

It isn't reachable so it is not part of the program? If you 
support generic programming you probably should limit proofs to 
reachable portions of library code.

However the specification or the implementation of it appears to 
be flawed, so perhaps it should be considered incorrect if this 
was in application code.

You usually try to prove post conditions in terms of pre 
conditions. The invariants, variants and asserts are just tools 
to get there. So this is not a typical issue.