On Saturday, 2 August 2014 at 20:27:09 UTC, Andrei Alexandrescu
wrote:
Hmmm... code that fails assertions is hardly working. -- Andrei
It is not the code that fails the assertion, it is the asserted
proposition that has not be satisfied by the axioms in the
program as it has been formulated in the context. It does not
mean "can not be satisfied", but "has not been satisfied".
The proposition and the code can be correct and still fail to
satisfy the proposition, if the axioms provided are insufficient.
Such as missing type info, deficiencies in the runtime, bugs in
the compiler, conditions in the environment++.
People who care a lot about correctness, that is, the guys that
do embedded system programming, have sane alternatives. Such as
compilers formally proven to follow the language spec of C:
http://compcert.inria.fr/
No D compiler is verified, thus it is a probable source for
missing or wrong axioms. Which in itself is a good reason to not
turn asserts into assumes. IF you need another one.
By turning programming by contract upside-down D basically kills
itself as a system programming language. The term "design by
contract" has implications. Turning the postconditions into
axioms is not one of them. Quite the opposite. I betcha a mean
lawyer would describe a compiler doing that with the phrase
"malicious intent"… and no copyright license can protect you from
that.
Telling people who want a system level programming language that
they should ship debug builds because release mode is dangerous
and has a high risk of violating the code if the annotations
cannot be met, for the sake of doing better local optimization
with a shitty backend isn't particularly encouraging. If I
wasn't looking for a system level programming language I'd think
it hilarious. But I don't. I think it is sad that the threshold
for taking advice is so high.
No sane person can claim D is aiming to be a safer language than
C++ after this debate.
