On Wednesday, 30 July 2014 at 12:11:31 UTC, Daniel Murphy wrote:
So you'll be happy if we call them D-style assertions?
Program verification has been at the core of CS for over 40
years. This is bachelor grade stuff. If you keep inventing your
own semantics for well-established terminology then nobody will
take D seriously.
For instance, if assert(false) is proven reachable then it means
either:
1. the specification is inconsistent/contradictory (thus wrong)
2. the program has been proved incorrect
The compiler should then refuse to generate code. If it is not
proven reachable then emitting HALT might be ok.
Basically D ought to allow a verifier to work on a D program,
then only emit runtime checks for asserts it cannot handle. And
also allow them to trigger as early as possible.