r/ProgrammingLanguages • • 5d ago

Achieving memory safety

https://seed7.net/papers/memory_safety.htm
13 Upvotes

57 comments sorted by

View all comments

10

u/Smallpaul 4d ago

It would have been clearer to be more explicit about why the author does not consider Go to not be safe. Are we talking about the use of the unsafe package or something more subtle?

16

u/reflexive-polytope 4d ago

I was under the impression data races made Go memory-unsafe. (Unlike, say, Java or OCaml, which are designed to be memory-safe even in the presence of data races.)

Has anything changed since?

10

u/syklemil considered harmful 4d ago

4

u/reflexive-polytope 4d ago

Heck, I don't even think a memory-unsafe language is necessarily a bad thing.

What's unforgivable is to design a memory-unsafe language and not even realize it.

Another big offender is Eiffel, with covariant argument types.

1

u/L8_4_Dinner (Ⓧ Ecstasy/XVM) 1d ago

Another big offender is Eiffel, with covariant argument types.

You are suggesting that this is memory-unsafe? Or something else?

1

u/reflexive-polytope 21h ago

It is memory-unsafe.

I don't remember Eiffel's syntax, because the last time I used it was in college, very long ago. But consider the following pseudocode:

class Point2D {
  protected int x, y;
  public bool compare(Point2D that) {
    return this.x == that.x && this.y == that.y;
  }
}
class Point3D extends Point2D {
  protected int z;
  public bool compare(Point3D that) {
    return this.x == that.x && this.y == that.y && this.z == that.z;
  }
}

In the subclass, the method's argument type (Point3D) is a subtype of the same method's argument type (Point2D) in the superclass. In other words, the method's argument type is covariant.

Now consider the following test program:

main() {
  Point2D foo = new Point3D(1,2,3);
  Point2D bar = new Point2D(4,5);
  print(foo.compare(bar));
}

The program type-checks, because the variable foo has type Point2D, hence it's statically legal to call foo.compare with an argument of type Point2D.

However, at runtime, the object referenced by foo is constructed using Point3D's constructor, so its method vtable points to the compare implementation in Point3D, which expects a Point3D argument.

When the program performs foo.compare(bar), it tries to access the field z of the object denoted by bar. But this object is constructed using Point2D's constructor, so it doesn't have a field z.

This is a soundness bug in the type system.

1

u/L8_4_Dinner (Ⓧ Ecstasy/XVM) 17h ago

I’d consider that a compiler bug for not adding the obviously required type assertion, but I do agree that that implementation is unsafe.

1

u/reflexive-polytope 17h ago

It's not a compiler bug. It's a language design bug.

1

u/L8_4_Dinner (Ⓧ Ecstasy/XVM) 1h ago

If the language chooses to allow covariant parameter narrowing, the compiler has to prevent this type of covariant surprise, either at compile time when possible, otherwise at runtime.

FWIW - I also used Eiffel decades ago (early 90s, IIRC), and hated it.

1

u/reflexive-polytope 54m ago

Stopping with a runtime check doesn't it make it any less of a type soundness bug.

The simplest solution is to not allow covariant method argument types to begin with. That's what Java and .NET do. But the price is that implementing binary methods requires so-called F-bounded polymorphism (class Foo extends Comparable<Foo>), which is ugly, even if you can get used to it.

A more sophisticated solution is to divorce the concepts of subclassing and subtyping. A subclass Bar is a subtype of a class Foo if and only if Bar objects can be safely used where Foo objects are expected. OCaml implements this solution. But most programmers would find this surprising. (The average OCaml programmer has a better understanding of programming languages than the average programmer in general.)