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