On Sunday, 25 July 2021 at 16:29:38 UTC, Bruce Carneal wrote:

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

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.

On Sunday, 25 July 2021 at 17:47:40 UTC, Paul Backus wrote:

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

So...

Call a safe function and get an int.
Use that int to index into an array with bounds checking turned off.

Wheres the memory safety bug? In the function that returns the int or in the system code that bypasses bounds checking?

So no that doesn't prove what you say it does, it doesn't mean favouriteNumber needs checking, it means the @system block needs checking. favouriteNumber knows nothing about the array length, to assume it does or it should is bad design.

On Sunday, 25 July 2021 at 20:36:09 UTC, claptrap wrote:

The questioner is what's at issue there, not the question.

Questioner #1: someone reviewing a patch that only changes the @safe function. This reviewer cannot determine from just the changes, to only @safe functions, that they won't cause the patched program to develop an out of bounds access. @safe/@trusted/@system is not really helping this questioner.

Questioner #2: someone reviewing a program with an out of bounds access. This reviewer doesn't have to examine @safe functions except when tracing the inputs to a @system block/function where they isolated the error. @safe/@trusted/@system has potentially saved this questioner a lot of time with getting an answer to "Where's the memory safety bug?"

On Sunday, 25 July 2021 at 17:47:40 UTC, Paul Backus wrote:

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

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.

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.

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.

On Sunday, 25 July 2021 at 20:36:09 UTC, claptrap wrote:

Strictly speaking, you're right; it is the @system block that needs checking, not favoriteNumber.

However, any time you change favoriteNumber, you have to re-check the @system block. From a maintenance perspective, this is no different from favoriteNumber itself requiring manual checking--if someone submits a PR that changes favoriteNumber, and you accept it without any manual review, you risk introducing a memory-safety bug.

The same logic applies to @trusted lambdas. Strictly speaking, it is the lambda that requires checking, not the surrounding @safe code. However, any changes to the surrounding code require you to re-check the lambda, so from a maintenance perspective, you must review changes to the @safe part just as carefully as changes to the @trusted part.

The underlying problem in both cases is that the memory safety of the manually-checked code (@system block/@trusted lambda) depends on details of the automatically-checked code that are not robust against change.

On Sunday, 25 July 2021 at 21:32:00 UTC, Paul Backus wrote:

Im sorry but it's nonsense.

You get an OOB error, it points you at the system block, you add bounds checking, job done.

Changing favouriteNumber doesnt introduce a bug, the bug was already there in the system block.

You cant expect favouriteNumber to be responsible for other code doing stupid things with its result.

On Sunday, 25 July 2021 at 21:32:00 UTC, Paul Backus wrote:

I think the problem is you're conflating memory safety and validity. When you slap @safe on favouriteNumber you're not telling the world that it will always return a valid result, you're telling the world that it wont corrupt memory.

IE.. @safe doesnt mean you can blindly use the result of a function.

EG.. if you have a @safe version of getchar(), would you blindly use the result of that?

On Sunday, 25 July 2021 at 22:05:26 UTC, claptrap wrote:

If the bug is "already there", you should be able to write a program that uses the unmodified versions of favoriteNumber and favoriteElement to cause undefined behavior in @safe code.

If you cannot, then you must admit that favoriteElement is memory safe as-written.

On Sunday, 25 July 2021 at 21:26:27 UTC, Bruce Carneal wrote:

Well, thanks, and good luck. I think if your DIP makes strong promises about how it will make the language much safer it is currently, that you'll see these same criticisms again about how potential safety actually remains the same.

If you make much more restrained claims, that "The name is the important change.", then any anticipated inconvenience with the rollout will seem to outweigh the benefit.

I recommend this justification for the DIP: what you are doing is rehabilitating @trusted functions, which are currently (for newbies) a bug-filled trap, and (for experts) disused in favor of @safe functions containing @trusted blocks. The language documentation tells people to use @trusted functions but the language in practice doesn't really have them.

That's simultaneously a humble change and one that substantially improves the language, vs. alternate proposal like "conform to Rust" that would add to D but leave it still having this @safe/@trusted/@system framework that doesn't work as intended.

People complain about "half-baked features" and here you would be proposing to bake this feature the rest of the way. That's a lot easier to support, and a more coherent language is something people can think about when they're having to touch a bunch of code as a result of the DIP changing the language.