On Sunday, 25 July 2021 at 16:29:38 UTC, Bruce Carneal wrote:
>Machine advantage comes in other forms. Firstly, we now have a properly segregated code base. @safe always means 'machine checkable'. Zero procedural @trusted code review errors in that now easily identified class.
I have already demonstrated that this is false. Here's my example from the previous thread on this topic, rewritten slightly to use the new-style @trusted
/@system
syntax from your proposal:
module example;
size_t favoriteNumber() @safe { return 42; }
int favoriteElement(ref int[50] array) @trusted
{
// This is memory safe because we know favoriteNumber returns 42
@system {
return array.ptr[favoriteNumber()];
}
}
I make the following claims:
- This code is memory-safe. No matter how you call
favoriteElement
, it will not result in undefined behavior, or allow undefined behavior to occur in@safe
code. favoriteNumber
is 100% machine-checkable@safe
code.- Changes to
favoriteNumber
must be manually reviewed in order to ensure they do not result in memory-safety violations.
The only way to ensure that @safe
code never requires manual review is to enforce coding standards that forbid functions like favoriteElement
from ever being merged in the first place.
One example of a set of coding standards that would reject favoriteElement
is:
- Every
@system
block must be accompanied by a comment containing a proof (formal or informal) of memory safety. - A memory-safety proof for a
@system
block may not rely on any knowledge about symbols defined outside the block other than- knowledge that is implied by their type signatures.
- knowledge that is implied by their documentation and/or any standards they are known to conform to.
favoriteElement
satisfies condition (1), but not condition (2)--there is nothing in favoriteNumber
's documentation or type signature that guarantees it will return 42.
I believe (though I cannot prove) that any set of coding standards capable of rejecting favoriteElement
under your proposal is also (mutatis mutandis) capable of rejecting favoriteElement
in the current language. If this were true, then the proposal would be of no value--we could simply implement those coding standards and reap their benefits right away, with no language changes required.
If you can give an example of a set of coding standards that rejects favoriteElement
under your proposal but fails to reject favoriteElement
in the D language as it currently exists, I would be very interested in seeing it.