assume, assert, enforce, @safe

[Timon Gehr via Digitalmars-d]

On 08/01/2014 04:58 PM, Andrei Alexandrescu wrote:
>>
>> assume:
>> passes a hint to the optimizer to allow better code generation.
>> is used when the expression is proven to be true (by the programmer,
>> like @trusted).
>
> There are a few corrections needed for "assert", i.e. "is a runtime
> check of the condition in debug mode". The whole "believed true but not
> proven so" is... odd, seeing as assert takes expressions that are
> considered tautological within the design,

Maybe _somebody_ does not know what the entire design actually is, or 
what all its implications are.

> and sometimes provable
> automatically (e.g. after inlining).
> ...

Sometimes.

> Anyhow, if "assume" is to be taken at face value the its semantics has
> always been what Walter intended for "assert".

Even then, such a semantics is non-standard and almost nobody else knew.
Why break 'assert' now, now that it actually behaves as I and many 
others expect (even some of those who argued for the (apparently, even 
inofficially) new and opposite design)?

> (Again "proven to be
> true" is an eyebrow raiser because when one thinks of "proof" of
> semantics of programs

I think he was using a very relaxed notion of proof, and he exemplified 
that by drawing an analogy to @trusted.

> one thinks of state analysis or progress and
> preservation and such.)

Progress and preservation are about soundness of the type system of the 
programming language, not program correctness. @safe may be seen to 
strive for progress and preservation conditional on it holding for 
@trusted functions. Your position has always been that @safe and 
@trusted represent a useful distinction, and this case is analogous (if 
different!).