Hacker News Reader

Comment by adamrezich | Hacker News Reader

There is no universally-accepted definition for the term "safe" as it applies to programming languages.

Actually, there is a rather pervasive notion of "soundness" in programming language theory. It has many flavors (because, as you hint, programming languages are quite varied). One of the most simple way of stating it, often dubbed "progress and preservation" is: a well typed program can execute (i.e., it doesn't crash) and returns a value of the same type.

This obviously covers type safety, but also spatial memory safety, and can be extended to temporal memory safety, and even some concurrency aspects.

This has been proven for fairly large subsets of programming languages and even some full languages (like SML). Unfortunately, it doesn't hold for most mainstream ones, because programming language theory is often ... under-used ... among language designers.

While we can of course always bikeshed the minutiae, memory safety is a fairly well accepted and well defined term. And so are temporal and spatial safety (as subsets of memory safety).

I would add that temporal safety is significantly harder than spatial safety (spatial safety is only hard in C if you do not want to break the ABI), so it is nice that this project is focusing on it.

This can simultaneously be true and for spatial memory safety to be a necessary condition of any coherent definition of “safe.”

True and yet useless. When "that's not safe" turns into a "discussion" about what safety means (e.g. at basically every C++ conference for over a year) what that signals is that you're much more interested in preserving the status quo than improving safety.

Alternatively, it signals that "safety" as a broad concept as it applies to programming languages, is pretty incoherent and ultimately useless.

"Safe" and "safety" are very overloaded English words that come with a lot of baggage, and perhaps it would be prudent to stop using these broad, nonspecific terms for things like programming languages.

"Memory safety" is a coherent, reasonably well-defined concept, and it's fine to talk about something like that. But what does a broadly, generically "safe" programming language even mean?

Oh! That's easy, although a little uncomfortable for some people.

A program is safe if it remains well-behaved regardless of inputs. A safe language necessarily constructs such programs. It turns out Memory Safety is a necessary part of this.

The reason this is awkward is that it turns out that languages such as Go do not meet this requirement because they exhibit UB under some data races. There are three ways out of this, which are interesting to contemplate

1. No concurrency. Languages which simply don't have concurrency are fine in this respect, e.g. Python, as are (so long as you don't try to have concurrency) older versions of C and even C++ which simply decline to explain how concurrency is even possible - if you're using say POSIX threads from C89 that's a problem because in C89 concurrency doesn't exist so none of your programs have any meaning whatsoever even if they don't race...

2. Rust's trick, mutation XOR multiple references - you can't write a data race in (safe) Rust, so even though the language has concurrency it's fine, you can't trip yourself this way.

3. Java and OCaml's trick, survive despite loss of Sequential Consistency. The proof we have is SC/DRF - using this construction a program is Sequentially Consistent if it is Data Race Free, but if we can survive loss of Sequential Consistency then this proof isn't important. This is enormously difficult, like it's easily the sort of work that could earn you a PhD if you don't have one already. We also still don't know whether it's potentially worth it. For Java the answer was "No" but for OCaml it's too early to say.

Edited to add: Marked that just not having concurrency only avoids data races, it doesn't magically fix all the other problems C and C++ have for example.

Reply on news.ycombinator.com