@system blocks and safer @trusted (ST) functions

[Steven Schveighoffer]

On Sunday, 25 July 2021 at 17:47:40 UTC, Paul Backus wrote:
> 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:
>
> ```d
> 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()];
>     }
> }
> ```

And I have [already 
demonstrated](https://forum.dlang.org/post/sag7fp$18oj$1@digitalmars.com), `favoriteElement` is invalid. You need to have a definition of what `favoriteNumber` does, and this needs to be reconciled with the definition of `favoriteElement`.

In this case, `favoriteElement` is invalid, because 
`favoriteNumber` has no formal specification. When reviewing 
`favoriteElement`, one must look at it like a black box:

```d
/// Returns: a valid size_t
size_t favoriteNumber() @safe;

int favoriteElement(ref int[50] array) @trusted
{ /* code to review */ }
```

However, with a specification of `favoriteNumber`, 
`favoriteElement` can be reviewed as correct:

```d
/// Returns: a size_t between 0 and 49, inclusive
size_t favoriteNumber() @safe;

...
```

Now, when reviewing `favoriteElement`, I can prove that it's a 
valid `@trusted` function given the formal definition of 
`favoriteNumber`. If reviewing `favoriteNumber`, I can reconcile 
the implementation changes against the spec for it, and know that 
as long as I follow the spec, I will not mess up any other code. 
If the spec changes, now you have to re-review anything that uses 
it (including other `@safe` code) for correctness.

As I said before, code reviews of `@safe` functions are still 
required for correctness, just not for memory safety.

-Steve