On Sunday, 25 July 2021 at 22:43:26 UTC, Paul Backus wrote:

Consider this...

int foo() { return 42; }

void bar()
{
int[2] what;
if (foo() == 24)
{
what.ptr[2] = 100; // BUG
}
}

Your argument the same as saying that bar() is memory safe as written. True, but it's not bug free. The bug is just waiting for the right set of circumstances to come to life and eat your face :)

IE. Memory safe as written != bug free

On Sunday, 25 July 2021 at 23:34:35 UTC, claptrap wrote:

Yes; I agree completely. :)

The point of the example is to show that the proposal advanced in this thread does not prevent this type of bug from occurring.

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

favoriteElement(), all on its own, has an unchecked type error: array is indexed by the int return value of favoriteNumber(), but int has a range outside of the 0..49 type of array's indices.

In Ada, array's index type would be specified in the code and you'd have to either perform a checked type conversion to use favoriteNumber() there, or you'd have to change favoriteNumber() to return the index type rather than an int.

with Ada.Text_IO; use Ada.Text_IO;

procedure FavElm is
   subtype Index is Integer range 0 .. 49;
   type Arg is array (Index) of Integer;

   function favoriteNumber return Index is (142);

   function favoriteElement(A : Arg) return Integer is
   begin
      return A (favoriteNumber);
   end favoriteElement;

   MyArray : Arg := (42 => 5, others => 0);
begin
   Put_Line (Natural'Image (favoriteElement (MyArray)));
end FavElm;

which compiles with a warning, and fails at runtime as promised:

favelm.adb:7:45: warning: value not in range of type "Index" defined at line 4
favelm.adb:7:45: warning: "Constraint_Error" will be raised at run time

In a language with dependent types (or the theorem-proving variant of Ada, SPARK) you could get a compile time error, including from functions that return statically unknown values that still have the wrong type, like getchar() as mentioned elsewhere.

In such languages the thing you should be doing, testing an int's range before using it as an index for an int[50] array, is a compile-time error to not do. You're not forced to check it at every index, but you have to check it at some point.

This kind of precision with types isn't so pleasant in D but the class of error is the same and it's something a reviewer could spot when initially checking this code in.

On Sunday, 25 July 2021 at 23:16:16 UTC, jfondren wrote:

The language doesn't have @trusted blocks. @trusted function literals (lambdas) are still functions. Everything the documentation says about @trusted functions applies to function literals.

People do like to treat @trusted function literals as if they were the proposed @system blocks. But then they're strictly speaking writing invalid code. They're cheating. And why not? It has significant advantages for the low price of (1) tainting some @safe code and (2) having a technically invalid program that works just fine in practice.

What the proposal does is turning the common cheat into an official part of the language, a best practice even. And the syntax gets a bit nicer.

On Monday, 26 July 2021 at 00:08:51 UTC, jfondren 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()];
    }
}

What if favoriteNumber originally returns a ubyte, and favoriteElement takes an int[256]?

ubyte favoriteNumber() @safe { return 42; }
int favoriteElement(ref int[256] array) @trusted
{
    return array.ptr[favoriteNumber()];
}

To your reviewer, there's nothing wrong with favoriteElement, right?

But later someone might change the return type of favoriteNumber to size_t and let it return 300. Badaboom: undefined behavior after touching @safe code. As far as I can tell, there's no way to truly make it impossible. Maybe disallowing calls to @safe functions from @trusted and @system code would do the trick, but that's impractical.

On Monday, 26 July 2021 at 00:37:36 UTC, ag0aep6g wrote:

ubyte favoriteNumber() @safe { return 42; }
int favoriteElement(ref int[256] array) @trusted
{
    return array.ptr[favoriteNumber()];
}

That's a much more obviously program-affecting change though, you're changing a function signature. It wouldn't make as compelling an example of someone being surprised that they have to review more than just a @safe function when that only that function is changed.

If you do name the index type then you can do something like this Nim translation of the Ada:

type
  Array = array[50, int]
  Index = range[0..49]

var myarray: Array
myarray[42] = 5

func favoriteNumber: Index = 42
func favoriteElement(arg: Array): int =
  let i: Index = favoriteNumber()
  return arg[i]

echo favoriteElement(myarray)

(But Nim disappoints here: if you change favoriteNumber to return an int, and then change the number to 142, then Nim doesn't complain at all about this code that assigns an int to a Index variable.)

On Monday, 26 July 2021 at 00:50:17 UTC, jfondren wrote:

The point stands: Changes to @safe code can compromise memory safety. Bruce claimed we would get "a properly segregated code base", and that @safe code would be entirely "machine checkable". But reviewers still have to be on the lookout for safety issues, even when no @trusted or @system code is touched.

On Monday, 26 July 2021 at 00:50:17 UTC, jfondren wrote:

Well, it still checks the indexing at runtime, just like Ada, Rust, C#, D, etc. One can do better than this and check it at compile-time but then you would complain about the annotation effort and implementation complexity so it would never stop to "disappoint"...