@system blocks and safer @trusted (ST) functions

Paul Backus snarwin at gmail.com
Sun Jul 25 17:47:40 UTC 2021

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 
     @system {
         return array.ptr[favoriteNumber()];

I make the following claims:

1. 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.
2. `favoriteNumber` is 100% machine-checkable `@safe` code.
3. 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:

1. Every `@system` block must be accompanied by a comment 
containing a proof (formal or informal) of memory safety.
2. 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.

More information about the Digitalmars-d mailing list