checkedint call removal

via Digitalmars-d digitalmars-d at puremagic.com
Sat Aug 2 14:25:39 PDT 2014


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.


More information about the Digitalmars-d mailing list