On 06/16/2014 01:06 AM, Walter Bright wrote:
On 6/15/2014 3:45 PM, Timon Gehr wrote:
I don't know why the documentation says that. D's @safe is about memory
safety, not undefined behavior.
...
Note that this is frustratingly unhelpful for deciphering your point
about
"memory safe" <=> "verifiably @safe" by definition. Are you defining
"memory
safe" or "verifiably @safe"?
I don't understand your question. I don't know what is unhelpful about
saying that @safe refers to memory safety.
...
You stated the two to be equivalent earlier, which is impossible.
Note that the list of eschewed behaviors are possibly memory corrupting.
It is an incomplete list.
I ask that you enumerate the missing items, put the list in bugzilla,
and tag them with the 'safe' keyword.
In any case, I
don't see how any list of (syntactic) verifiable properties of the
code is
supposed to be equivalent to the (non-trivial semantic) memory safety
property.
The list is not restricted to syntactic issues.
...
(Yes it is, but that is not important because here the problem here is
clearly that these terms have wildly different meanings in different
communities.)
The important distinction is between verifiable and non-verifiable.
@safe cannot be equivalent to memory safe because @safe is verifiable
and memory safe is not.
Are you assuming @trusted as an oracle for memory safety and saying
@trusted
code is 'verifiably @safe' code? (That's not the intended reading.)
Not at all. Where does the spec suggest that?
...
I'm just trying to find the definition/theorem we do not agree on.
Signed integer overflow, for example, is not listed.
Are you trying to say that signed integer overflow is undefined
behaviour in D?
(This would again contradict the documentation.)
I know the spec says it follows 2's complement arithmetic. I'm not 100%
confident we can rely on that for all 2's complement CPUs, and
furthermore we have a bit of a problem in relying on optimizers built
for C/C++ which rely on it being undefined behavior.
In any case, it is still not an issue for @safe.
Maybe not in practice (though I'll not bet on it), but a conforming
implementation can do _anything at all_ if undefined behaviour occurs,
including behaving as if memory had been corrupted.
