"Ola Fosheim Grøstad" " wrote in message
news:[email protected]...
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.
It sure seems easy to make D not be taken seriously. Every day somebody's
making this claim about something.
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.
You say this as if it's a law of physics. One of the great things about
working on D is that we get to assign the semantics that we decide are most
useful, and don't have to follow what other people have done.
A good example is D's purity. It doesn't match traditional definitions of
purity, but it's useful. I'm sure that's another reason not to take D
seriously.
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.
You're just saying it should work the way you think it should work. The
fact that other people have defined it that way before does not outweigh the
value of defining assert the way I've described IMO. I don't think the
safety concerns are warranted either, due to the existing optimizer
precedent.
Any verifier for D would have to understand the semantics of D's assert. If
the verifier assumes asserts are always replaced with a runtime check, then
it will be fine as long as you don't compile with -release.
