@system blocks and safer @trusted (ST) functions

[Bruce Carneal]

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()];
>     }
> }
> ```
>
> 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.

OK, I think I see where we're diverging.  I never thought that 
any automated checking could absolve the programmer from actually 
understanding the code.


>
> 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.
>

There is no way to ensure/prove anything if you are ignorant of 
the code so per such a framing we can assert, trivially again, 
that the only way of avoiding "manual review" (reading) is to 
disallow the code.


> One example of a set of coding standards that would reject 
> `favoriteElement` is:
>
> ...
>
> 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.

Unless I'm really missing something, nothing interesting is being 
proven or disproven here beyond the importance of definitions 
when "proving" things.

I'd like to conclude with two points from the beerconf discussion 
on this proposal, first your excellant observation that @trusted 
might be viewed as the @safe <==> @system programming analog of 
"weakly pure": it's where some good degree of localization might 
occur but where interesting stuff also gets done.  That @safe 
actually might be profitably "purified" of the dreaded trusted 
lambda! :-)

Secondly, there was a history-of-the-ideas-embodied-in-the-DIP 
put together nicely by Joe Wakeling that indicates several 
possible "origination points" for the ideas.

Further posts are welcome but Joe and I are going mostly quiet 
now, aiming for a concentrated DIP effort very late in the year.