assume, assert, enforce, @safe

[David Nadlinger via Digitalmars-d]

On Thursday, 31 July 2014 at 21:25:25 UTC, Walter Bright wrote:
> On 7/31/2014 1:33 PM, David Nadlinger wrote:
>> I've had the questionable pleasure of tracking down a couple 
>> of related issues
>> in LLVM and the LDC codegen, so please take my word for it: 
>> Requiring any
>> particular behavior such as halting in a case that can be 
>> assumed to be
>> unreachable is at odds with how the term "unreachable" is used 
>> in the wild – at
>> least in projects like GCC and LLVM.
>
> For example:
>
>  int foo() {
>    while (...) {
>        ...
>    }
>    assert(0);
>  }
>
> the compiler needn't issue an error at the end "no return value 
> for foo()" because it can assume it never got there.
>
> I'll rewrite that bit in the spec as it is clearly causing 
> confusion.

Don't rewrite it because you merely concede that it might be 
confusing. Rewrite it because you admit it's contradictory. If 
you just try to reword the spec without understanding how your 
use of the terminology differs from the established meaning, 
you'll probably come up with something that is confusing to the 
rest of the world just as well.

Perhaps looking at the situation in terms of basic blocks and the 
associated control flow graph will help:

As per your above post, assert(0) has nothing to do with making 
any assumptions on the compiler side. It merely servers as a 
terminator instruction of a BB, making it a leaf in the CFG. This 
seems to be the definition you intend for the spec. Maybe add 
something along the lines of "behaves like a function call that 
never returns" as an explanation to make it easier to understand.

This is not what "unreachable" means. If assert(0) was 
unreachable, then the compiler would be free to assume that no 
CFG edges *into* the BB holding the instruction are ever taken 
(and as a corollary, it could also decide not emit any code for 
it). Thus, the term certainly shouldn't appear anywhere near 
assert(0) in the spec, except to point out the difference.

Cheers,
David