July 25, 2021

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

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.

July 25, 2021

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

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.

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.

July 25, 2021

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

>

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?

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?"

July 25, 2021

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

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.

July 25, 2021

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

>

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.

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.

July 25, 2021
On 7/25/21 10:43 AM, Joseph Rushton Wakeling wrote:

> On Sunday, 25 July 2021 at 05:05:44 UTC, Bruce Carneal wrote:
>> At beerconf I committed to putting forward a DIP regarding a new
>> syntactic element to be made available within @trusted functions, the
>> @system block.  The presence of one or more @system blocks would
>> enable @safe checking elsewhere in the enclosing @trusted function.
>
> 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.

In a recent discussion, I learned from you an idea of Steven Schveighoffer. Add to that the relayed opinion of an academic to the effect of "it is not safe if you can escape out of it." And add to that our failed attempt at "safe by default", the following thought formed in my mind.

This thought may be exactly what Steven Schveighoffer or Bruce Carneal are bringing up anyway. If so, sorry for only now understanding it. :)


The problems:

1) @system by default provides no checking by default

2) @trusted is not checked either

3) @safe is not safe because you can escape easily


How about:

1) Make @trusted the default

2) Change @trusted's semantics to be safe (i.e. make it the same as today's @safe)

3) Allow @system inside @trusted

4) Strengthen @safe: No @trusted or @system allowed


Result:

1) We have safe by default because now @trusted is the default and trusted is checked by default

2) @safe is actually safe; no embarrassment


Existing code:

1) Replace @safe keywords with @trusted where the compiler complains. (No safety lost because @trusted will be behaving exactly like today's @safe.)

2) Add @system where the compiler complains. This is because all code is @trusted by default and @trusted is safe.

Ali

July 25, 2021

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

>

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

>

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.

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.

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.

July 25, 2021

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

>

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.

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?

July 25, 2021

On Sunday, 25 July 2021 at 22:05:26 UTC, claptrap 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.

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.

July 25, 2021

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

>

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

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.