On Sunday, 25 July 2021 at 13:19:55 UTC, Paul Backus wrote:

There is no getting away from manually checking the @system block(s) so (2) would be , IIUC, just as it is now wrt compiler assumptions.

The improvements on the status quo include the ability to easily delimit "should check very closely" code and the corresponding ability to engage @safety checking on any remainder.

Yes.

Yes. As Walter has put this, we'd be forcing args/operands to "come in through the front door" rather than sneaking in the back.

On Sunday, 25 July 2021 at 13:55:14 UTC, Bruce Carneal wrote:

We already have this ability: simply avoid writing @trusted code whose safety depends on out-of-band knowledge about @safe code, and enforce this practice via code review.

As I've discussed previously [1], there is no way to enforce this at the language level, because the language does not (and cannot possibly) know what knowledge @trusted code depends on for its memory safety.

[1] https://forum.dlang.org/post/auqcjtbbamviembvcaps@forum.dlang.org

On Sunday, 25 July 2021 at 13:42:52 UTC, Paul Backus wrote:

I do not know of any competent programmer who would say otherwise.

I also do not know what this has to do with a discussion regarding debasing/improving @safe. What am I missing?

On Sunday, 25 July 2021 at 14:13:45 UTC, Paul Backus wrote:

I'd like to have assistance from the compiler to the maximum extent possible and then conduct the code review(s). Assuming low (near zero) false positives out of the compiler, I'm not sure why one would prefer manual checking when compiler checking was available, but that option is certainly available in both the current and proposed environments.

On Sunday, 25 July 2021 at 14:19:47 UTC, Bruce Carneal wrote:

It is a response to the claim that "the compiler's assertions regarding your remaining @safe code might actually mean something." They mean exactly the same thing with your proposal as they do without it: that the @safe portion of the program does not violate the language's memory-safety invariants directly.

On Sunday, 25 July 2021 at 14:34:27 UTC, Bruce Carneal wrote:

Under your proposal, the proportion of code that must be manually-checked vs. compiler-checked does not change at all.

On Sunday, 25 July 2021 at 14:36:27 UTC, Paul Backus wrote:

They don't mean the same thing to me. In one case @safe invariants are asserted with a process that limits human error to group-visible forms (compiler errors in the code handling @safe). In the other case we add in a more direct form of human error, the failure to correctly review "@safe" code that contains trusted lambdas.

In one case, your @safe code comes in one flavor, machine checkable. In the other case your @safe code comes in two flavors, machine checkable and needs-human-intervention since you have no opportunity to segregate to the new @trusted form.

On Sunday, 25 July 2021 at 13:19:55 UTC, Paul Backus wrote:

4 kinds.

Split this into:

1. Code that is automatically checked for memory safety.
   1a. Code that has portions that have mechanical checks, but overall still needs manual checking for memory safety.

(1) and (1a) are marked @safe. The latter have @trusted lambdas but require manual verification. The difference between 1 and 1a is pretty subtle.

Under this proposal (though I haven't seen exactly the proposal, but I think I've conversed with Bruce enough to have a good understanding), 1 becomes @safe exclusively (which is the main benefit), 1a becomes @trusted, 2 becomes legacy (marked @trusted but with no @system escapes) and IMO should be warned about to the user, 3 is still @system.

This doesn't solve the problem exactly. A @trusted lambda is a localized piece of code, and is prone to be abused with the justification "well, it's just for this one time, and I know what this function does". The compiler cannot enforce that the code inside (current) @trusted functions actually obeys the @safe API.

No, it shouldn't be. The idea is that @trusted code without @system escapes is still accepted as legacy code that works as before. I would recommend a message from the compiler though.

@trusted lambdas should be required to be static, though that still doesn't solve the abuse problem. Perhaps they should just be disallowed?

-Steve

On Sunday, 25 July 2021 at 14:38:18 UTC, Paul Backus wrote:

The direct translation of an embedded lambda @safe function to the corresponding trusted/@system leaves you with the exact same amount of work at the point of translation wrt that function, without dispute.

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.

Another possible benefit (hypothesis only here) is the ease with which existing @trusted code can be made @safer. External clients already believe that you're @trusted, so at any time you can become @safer, incrementally (shrink the, initially large, @system block(s)). More machine checking available along a reduced friction path. TBD.

Another possible benefit (bigger leap of faith here) is that the continuously-variable-safety mechanism will encourage safer coding generally by reducing the friction of moving functions the other way, from @system code to @safer trusted. More machine checking available along a reduced friction path. Again, TBD.

Another possible benefit is that all new @trusted code would start with a form that defaults to @safe (you opt out). I think that defaults matter and that this one would lead to more machine checkability passively,or "by default". No need to wait for the "right" time to move to @safe with @trusted escape, just evolve the code.

Architecture matters more here than the exact forms most would say, and I'd mostly agree, but I believe the forms are important.

I also believe that there are other benefits, primarily in terms of human visuals (more easily discerned and more easily localizable @system regions) but the above are what come to mind wrt machine checkability.

I'm still thinking about it. It's less work if this is destroyed, so keep those sharp critiques coming! :-)

On Sunday, 25 July 2021 at 05:05:44 UTC, Bruce Carneal wrote:

I'm very happy to hear that. I think this proposal is an important and useful one, and I have been thinking of volunteering to write a DIP myself on the topic. I'll be dropping into tonight's BeerConf in a little while, so hopefully we can touch base then and see if we can find an opportunity for collaboration (maybe two heads and two people's spare time can overcome that burden of effort more readily than one).