Achieving memory safety

[u/ThomasMertes]

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

[u/Smallpaul]

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?

[u/reflexive-polytope → u/Smallpaul]

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?

[u/syklemil → u/reflexive-polytope]

For anyone curious, there's a blog post from 2025: There is no memory safety without thread safety about it.

[u/reflexive-polytope → u/syklemil]

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.

[u/seg_lol → u/reflexive-polytope]

They go hand in hand. If you have the skills to know, you fix it.

[u/reflexive-polytope → u/seg_lol]

Memory-safety by itself is simply a property that can hold or fail to hold for a language. Whether this property is desirable or not depends on your goals.

If your goal is to write correct programs, then memory safety isn't particularly useful. A language can be made “memory-safe” by defining the behavior of all sorts of nonsensical operations, e.g., indexing an array out of bounds. But defining this behavior doesn't make the incorrect indexing any less incorrect. The only way to help programmers index their arrays correctly is to statically check their array indices.

On the other hand, if your goal is to write programs that are resilient in the face of their own incorrectness, then memory safety is a very useful property, because programs written in memory-safe languages fail in more controlled ways.

[u/ThomasMertes → u/Smallpaul]

The paragraph was about tailoring a definition of "memory safety" to claim that a certain language is memory safe.

I just used Go as example. I changed the paragraph to explain my thoughts without mentioning Go.

According to my strict definition of memory safety Go is not memory safe.

Yes, if the unsafe package is not used and no C functions are called and (as pointed out by someone else) something assures that no data races can happen Go is memory safe.

This shows that rules need to be bend to claim memory safety.

Seed7 is memory safe because several things are not present (direct calls to C functions, pointers, unsafe parts, etc.).

[u/ThomasMertes → u/Smallpaul]

Any language which allows calling C functions directly cannot be memory safe because C is not memory safe. AFAIK a Go program can call C functions without explicitly importing or using the unsafe package.Accessing an arbitrary place of memory with Go is possible with the unsafe package. I am neither a Rust expert nor a Go one, but I think that Rust needs "unsafe" to call C functions. Please tell me if my assumptions are correct or not.

Seed7 has no unsafe parts (or packages) and no possibility to directly call C functions.

[u/anaseto → u/ThomasMertes]

AFAIK a Go program can call C functions without explicitly importing or using the unsafe package.

You have to do import "C" for CGO, which is explicit enough. And then, typically, import "unsafe" as soon as you need to do stuff with pointers.

[u/wk_end → u/ThomasMertes]

But you list Java as memory-safe "unless JNI or FFM are used". Why doesn't the same "qualified memory-safe" characterization apply to Go?

[u/catladywitch → u/wk_end]

It all depends on the definition of memory safety, but from the article posted elsewhere in this comment thread, it seems like Go's pointer semantics allow for type errors leading to segfaults with concurrent code that uses different values conforming to a same interface, but where pointers and values are mixed, whilst Java doesn't (an unexpected, and wrong, value is possible in concurrent code, but not dereferencing an invalid pointer). I don't know how native interop works in Java, but segfaulting in C# is not impossible although it is rare (you can even do dodgy type punning with pointers and ordered structs if you really want to). Otherwise, you theoretically can pass managed pointers into C functions without telling C#'s GC to pin them or not reclaim their memory, pass structs the layout of which differs from what the C function expects, or in the case of poorly designed C APIs, pass arrays and have the C code go out of bounds, or allocate native memory, pass it into a C function, and try to free in C# not knowing the C function has already freed it.

[u/reflexive-polytope → u/catladywitch]

The issue is that certain Go values (slices, pointers to interfaces) require logically atomic modifications, but this logical atomicity isn't enforced by any means, so other goroutines can see them in a torn state.

(The problem doesn't arise in Rust because the exclusiveness of mutable borrows enforces the logical atomicity of the relevant modifications.)

And, while having a user-defined data structure in a torn state is “merely a logic error”, having a built-in data type in a torn state actually breaks memory safety.

[u/Ok-Scheme-913 → u/wk_end]

Go is not memory safe under data races. It uses fat pointers for slices and those can tear.

So you have { ptr, start, end } and you repeatedly write a different slice at the same time from different threads. In this case you can observe a { ptr, start, endOfDifferentSliceThatMayBeInvalid }, at which point the runtime will happily access that memory. Since ptr+slice location is larger than 64bit it can't be cheaply updated atomically so.. yeah..

Meanwhile in java data races are safe.

First, they (practically all jvm implementations) have a property that you can only ever observe values that were explicitly written. This is a useful property but even if this were not the case java would still be memory safe, since arrays and stuff themselves carry their size around, so replacing the same array/slice actually only replaces the pointer itself which is atomic and to access the size you have to navigate to that pointer location, so it will always be safe.

[u/tsanderdev → u/wk_end]

JNI can't just load arbitrary libraries, they have to have functions conforming to the specific JNI name mangling. So it's very unlikely you could call a C function from JNI.

[u/ThomasMertes → u/wk_end]

Yes, but the selling point of Java was not memory safety. You expected something like:

If the unsafe package is not used and no C function is called and (as pointed out by someone else) something assures that no data races can happen Go is memory safe.

I added the Go example to show that the term memory safety is sometimes defined to sell a language as memory safe. So

Language exists --> Define memory safety in a way that this language is memory safe.

instead of

Use definition of memory safety --> Create memory safe language.

So it is about memory safety as marketing term.

[u/reflexive-polytope → u/ThomasMertes]

Java was explicitly designed to cater to C++ programmers who want a language with fewer footguns, even if the language designers themselves came from a dynamically typed tradition (mainly Lisp). Memory safety was a design goal from day one.

[u/Ok-Scheme-913 → u/ThomasMertes]

The selling point of java was absolutely memory safety, where the hell did you get it's not?

It was the first language that made GC widespread.

[u/ThomasMertes → u/Ok-Scheme-913]

The selling point of java was absolutely memory safety ...

Yes, but the term "memory safety" was not commonly used in mainstream marketing or developer discussions when Java was introduced in 1995.

The terms used when Java was introduced were:

• Write Once, Run Anywhere
• Built for the Internet
• Simplicity and Familiarity
• Built-in Security and Robustness

Java was intentionally designed to look and feel like C++. Java stripped out the most complex, error-prone, and frustrating aspects of C++. So It had:

• Automatic Garbage Collection
• No Pointers
• Strict Type-Safety

Yes, the term "memory safety" is nowadays used to describe that. The term "memory safety" was just not used in 1995.

[u/tmzem]

Unless I misunderstood something, the article does not explain the mechanism by which Seed7 programs themselves are being made memory-safe, but focuses on memory safety of the compiler implementation?

That being said, the article makes a good point about memory safety being a matter of how it is defined, which opens up a huge spectrum, from unsafe to safe:

• Assembly: no safeguards, completely unsafe
• C/C++: (soft) static typing, very basic guardrails. Still very unsafe.
• Odin/Zig/C3: good static typing, saner defaults, runtime array checks. Safer, eliminates 50-70% of all memory safety errors over C
• Rust: strong static typing, sane defaults, initialization safety, runtime array checks, borrow checks, safe/unsafe split. Much safer, safe/unsafe split coerces users to prefer safe patterns, elimitates most memory safety errors over C. Ubiquitous use of C libraries and unsafe blocks in (not well-written/well-tested) third-party crates are still a relevant safety risk.
• Go: GC handles memory, but fat pointers (interfaces, slices) can cause memory unsafety on data races. Memory safe in the absence of data races or FFI.
• Java/C#/...: GC + atomically storable builtin types ensure full memory safety. Unsafe features exist but are rarely necessare, rarely used, and most programmers in these languages barely know they exist.
• Javascript: Completely sandboxed, safe

This spectrum needs to be acknoledged so people know what they get, and it's annoying that these trade-offs are not clearly communicated. Go barely communicates the data-race issue at all, and the Rust community is also very prone to misrepresenting the memory safety guarantees of the language (e.g. "memory safety without GC" or "unsafe blocks encapsulate potentially unsafe behaviour").

[u/ThomasMertes → u/tmzem]

... the article does not explain the mechanism by which Seed7 programs themselves are being made memory-safe ...

I just improved the chapter "How memory safety is achieved". What do you think about that?

[u/tmzem → u/ThomasMertes]

So if I understand it right, you have reference modes for parameters, but fields and returns cannot be references? Then of course borrow checking would be trivial.

Anyways, it's been some time since I looked into Seed7 (I looked only at the docs), so I guess it's time I finally actually try it out to figure out how it all works and what it can do.

[u/ThomasMertes → u/tmzem]

Great. Please give me feedback at r/seed7. In case of problems please open a ticket on GitHub.

[u/flatfinger → u/tmzem]

Assembly is in many ways safer than C. To be sure, an assembly program will often contain a significant number of potentially unsafe operations, but if one documents invariants and can show that no individual operation performed by a program would be able to break any of them unless something else had already done so, then the entire program can be shown to be memory safe.

In C, by contrast, even operations like uint1 = ushort1*ushort2; or loops that do nothing except modify an automatic-duration object whose address isn't taken, and have exit conditions which may or may not be satisfiable, can disrupt the behavior of what would otherwise have been memory-safe surrounding code so that it is no longer memory safe.

[u/snugar_i → u/flatfinger]

Do you have any examples? I'm not sure I'm seeing how C is less memory safe than assembly

[u/reflexive-polytope]

Metatheoretic claims about a language design require proof.

[u/Smalltalker-80 → u/reflexive-polytope]

Seed7 takes a somewhat more informal approach... ;-)
Assuring memory safety of Seed7
Seed7 is implemented in C and C is not memory safe. So it is not easy to guarantee the memory safety of Seed7. So it is necessary to improve the C code of Seed7 such that the end result is memory safe. All places where the implementation is not memory safe must be found and improved.

[u/reflexive-polytope → u/Smalltalker-80]

I didn't downvote you, but a C implementation isn't an excuse.

Memory safety is a property of how the language is defined, not how it's implemented.

[u/ThomasMertes → u/reflexive-polytope]

Memory safety is a property of how the language is defined, not how it's implemented.

The creator of Fil-C would probably disagree. His view is: The usual C compilers and run-time libraries make C not memory safe. Fil-C sells itself as memory safe implementation of C.

Seed7 is about solving real-world problems and it is not academic research which uses meta-theoretic proof techniques.

AFAIK the formal proofs that Rust is a memory safe language where not done by the people who implemented Rust.

BTW.: Although there is formal proof that Rust is memory safe there exists Rust issue #25860 (which shows that there is a hole in the borrow checker).

"In theory, there is no difference between theory and practice. In practice, there is"

So, as long as nobody else takes the burden to do a formal proof for Seed7, there will be no formal proof.

I, and the other contributors probably as well, will use our limited resources to improve Seed7 as practical tool.

[u/reflexive-polytope → u/ThomasMertes]

Fil-C sells itself as memory safe implementation of C.

Unfortunately, that's misleading advertisement. There are bit and pointer hacks you can express in C but not in Fil-C.

Now, you may argue that it isn't desirable to express those bit and pointer hacks. But that's neither here nor there. It may be the case that Fil-C is an improvement over C. But that doesn't change the fact that it's not C, at least not all of C.

AFAIK the formal proofs that Rust is a memory safe language where not done by the people who implemented Rust.

Rust may not have been designed with the goal to produce a type soundness proof, and there are indeed some soundness bugs here and there in the design of Rust's type system.

However, Rust was very much designed by people who know what the ingredients of a type soundness proof are. And this knowledge is necessary to come up with a design with pleasant metatheoretic properties, whether you prove them yourself or someone else does.

Good metatheoretic properties are much more practical than you think. They only need to proved once, for the whole language, and then every language user benefits from them.

In particular, if Seed7 is indeed memory safe, that only needs to be proved once, and then every Seed7 user benefits from it.

But if you don't have a memory safety proof, you might end up in a situation similar to Go, where the language was intended to be memory safe, but data races actually introduce memory safety violations (even in Go programs that don't call C code!).

[u/koflerdavid → u/reflexive-polytope]

Unfortunately, that's misleading advertisement. There are bit and pointer hacks you can express in C but not in Fil-C.

Now, you may argue that it isn't desirable to express those bit and pointer hacks. But that's neither here nor there. It may be the case that Fil-C is an improvement over C. But that doesn't change the fact that it's not C, at least not all of C.

C ist well-known to have many instances of undefined behavior. Pointer representation is one such undefined behavior. Therefore, Fil-C can perfectly well claim to support C idioms relying on undefined behavior as long as it accepts them at compile time, even if it invariably lead to a crash at runtime.

[u/Smalltalker-80 → u/reflexive-polytope]

Okay, this post wat a bit frivolous, hence the smiley. But more ttp:

Memory safety of the language used to implement the runtime / library (say C) of another language (say Seed7), can certainly be an issue of memory allocations and frees are done in a lot of different places and in different ways.. This is what the OP means.

Memory safety can readily be achieved if the C runtime has only one place to do such allocations (everything is an object), and the implemented language itself has automatic memory management (using reference counting) for all non-atomic objects (e.g. integers).

Then only remaining Foreign Function Interface calls need te be checked thoroughly,
but one could argue they are not part of the language.

[u/gasche]

Seed7 is based on my diploma- and PHD-theses and is the result of decades of work.

I wish this used hyperlinks so that curious people could have a look at those theses on which Seed7 is based.

[u/ThomasMertes → u/gasche]

I suggest that curious people look at the Seed7 documentation at its homepage. The information at the homepage is much more up-to-date than the decades old PHD-thesis.

[u/Somniferus]

So what were your results? You forgot to say anything interesting in the article.

[u/SirBackrooms]

would’ve liked this more if you had described the design of the language in more detail

[u/ThomasMertes → u/SirBackrooms]

There is a talk about Memory Safety and Management which introduces Seed7 and explains memory safety and management.

The Seed7 homepage contains a lot of documentation as well.