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:
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, 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:
/// 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:
/// 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