SPARK has had it before Rust existed. However, gnatprove doesn't require you the programmer to change anything. The compiler does the work to ensure safety, not you.

Oberon is similar. The typesolver will determine if something is safe, without the need for explicitly borrowing anything.

> Oberon is similar. The typesolver will determine if something is safe, without the need for explicitly borrowing anything.

so what does oberon do to prevent you from resizing a possibly reallocating array while holding a reference into it?

It doesn't allow those operations to occur at the same time. If you can't meet compile time guarantees, then it does not compile.

Pointers aren't the same as in C. A pointer has an explicity type, not just a size. A pointer cannot change where it is located, whilst in scope anywhere else.

If you then make your pointer local, then it will get cloned. As there's no concept of a void pointer, every type supports cloning, and so your thread-local variable will have nothing to do with the parent any longer.

So if you try to grab a local reference, to something in another thread, you'll get a copy, or a compile time error if you don't copy it.

If you try to modify something you're looping over, it won't compile at all.

However, in all of this, there's no extra syntax. The compiler can deal with what is permitted. The programmer can just write.

This is multithreaded (by compiler switch):

        module example610a;
        type
        Vector = array * of integer;
        var
          i, n: integer;
          a: Vector;
        begin
          a := new Vector(n);
          for i := 0 to len(a) - 1 do
            write("a[",i:2,"]: "); read(a[i])
          end;
          writeln;
          for i := 0 to len(a) - 1 do
            write(a[i]:3);
          end;
        writeln;
        end example610a.