These should be table stakes when talking about "safe" languages (or subsets thereof); I hope these authors have or propose plans for these classes as well!
(I agree with the more general critique here, that any adaptation invasive enough to provide these properties in C might as well be its own programming language.)
Xr0 is not limited to memory-safety, its goal is to eliminate the possibility of writing C code that results in undefined behaviour. A good analogy can be drawn to how Typescript wraps Javascript and provides type safety. Think of Xr0 as a wrapper to C that guarantees you don't violate C's safety semantics.
Like this idea a lot. Does that mean it could be used to convert C projects in a strangler pattern style?
(Other proposals that I’m aware of seek to forbid those parts of the language outright, or add some kind of runtime instrumentation like isoheaps. Neither of these is particularly palatable for pre-existing codebases with deep, undocumented language feature and ABI assumptions!)
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.
"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?
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.
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.