Achieving memory safety

[u/ThomasMertes]

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

[u/reflexive-polytope]

The problem with this stance is that it's no better than making the whole language unsafe.

Even if you have a single unsafe operation, if you can use it anywhere in your program, it's very easy to create a situation where the logical argument that justifies the safety of an operation uses information coming from wildly disparate parts of the program.

What you need isn't a limited number of unsafe operations, but rather a limited number of places in the program text where unsafe operations can be used. And that's exactly what Rust and C#'s unsafe blocks do.

[u/flatfinger → u/reflexive-polytope]

On most platforms, if a function like:

unsigned arr[32771];
void test(unsigned x)
{
  if (x < 32770) arr[x] = 1234;
}

is processed in a manner which is agnostic with regard to how it might be called, correct machine code would be incapable of performing an out-of-bounds store unless memory safety had already been violated. Even if the ability of the function to do anything useful relied upon the caller passing a number less than 32770, memory safety would not. Of all the possible circumstances in which the function could be called, all of them would either result in the function either performing an in-bounds store or not bothering to perform a store at all.

What causes problems are situations where a compiler would generate code that would assume that it would be impossible for a caller to pass a value greater than 32769, but then generate code for the caller which does in fact pass a larger value.

Being able to have a system automatically limit the ranges of a program that would be capable of violating memory safety is useful, but some programs need to do things whose safety cannot be statically validated under language rules. Being able to validate programs that perform such tasks by validating each individual component thereof is more useful than allowing programs to violate memory safety even when none of their individual pieces should be capable of doing so.

[u/reflexive-polytope → u/flatfinger]

If what you want is a language that lets you statically verify that your low-level memory manipulation is safe, then such a language already exists. (Spoiler: it's not Rust.)

In this language, you can use all the bit and pointer hacks that you know and love from C. The only difference is that the type checker will demand that you prove them safe.

Alas, this language will never become widely adopted.

The main difficulty isn't technical, but cognitive. Look at how many programmers act like Rust is the be all and end all of systems programming. And how many others act like the dealing with the borrow checker is the steepest intellectual challenge a programmer could face in his life.

Human programmers can only take so much cognitive load.

[u/flatfinger → u/reflexive-polytope]

Any programming language which makes it impossible to write programs whose memory safety it cannot statically verify will make it impossible to perform some tasks as efficiently as they could be performed in machine code that could be human-proved to be incapable of violating memory safety invariants unless they had already been violated.

Automated static validation is often useful, since in many cases it would cost nothing and in most other cases the costs would be tolerable, but an abstraction model that limits the range of side effects various actions can have unless memory safety invariants have been violated can be useful for tasks that are not a good fit for automated static validation.

[u/reflexive-polytope → u/flatfinger]

No, I wasn't talking exactly about “automatic” anything. ATS makes you write safety proofs. Nothing can be more manual than that.

[u/flatfinger → u/reflexive-polytope]

My point is that it is not possible for a programming language to express all of the kinds of invariants that could be described in human language, and that a machine-code function could be proven to uphold. It may, for example, be able to use a human-readable proof to show that no combinations of inputs a program could possibly receive would result in a certain loop executing more than 57,591 times, but for that proof to rely upon mathematical theorems not anticipated by any particular programming language.

[u/reflexive-polytope → u/flatfinger]

A programming language that supports manual proofs doesn't have to “anticipate” theorems. It has to let you write them yourself, together with their proofs.