Xr0 Makes C Safer than Rust
xr0.dev
xr0.dev
Instead, I think something like "Makes C safer than the C code you were using previously" is the better approach.
I haven't read every detail of this long post, but I do want to highlight something I strongly agree with:
> Interface informality is the root cause of unsafety
When writing C and C++, I've always felt an uneasy when passing a pointer to a function, because I don't really have a way of knowing if this is safe or not.
The comparison is not meant antagonistically, but almost as tongue-in-cheek.
In making the comparison we're acknowledging that Rust is the touchstone for safety in today's (programming) world. Our praise for Rust in the article shows this.
Rust also statically prevents race conditions in multi-threaded code, via the Send and Sync traits. This blog post describes annotations which make Xr0 a safer dialect of C, but its still far less safe than rust.
This looks like a cool project, but I've gotta agree with other commenters. The blog post title is a false promise. If you think the project is good (and it looks good!), then why lie about its capabilities?
The fundamental problem with fixing C/C++ is that you have to take stuff out of the language to make it safer. That's not going to happen.
The trouble with going to Rust is that the language is so different from C/C++ that conversion is tough, both for code and for programmers. It's not the syntax. It's the semantics of affine types. Strict single ownership requires a major rethink of program organization. The result is, arguably, better programs. But it's a wrenching change. Interlinked data types have to be completely redesigned.
(There are people trying to fix that problem in Rust. There's "Arc::new_cyclic", which lets you have weak backlinks. Now you can find your parent in the hierarchy, which means you can do object-like things if you want to. There's also UniqueRc in development.[1] There's the theoretical possibility of proving at compile time that no .upgrade() operation on such objects will result in a failure due to two strong pointers existing at the same time. If that could be done, the reference counts could be eliminated and Rust would have safe back-references. Nobody has figured out how to do that yet. So for now, the mismatch between C/C++ and Rust is pretty bad.)
Yes, Xr0 is young. It took Rust nine years to reach v1.0.0. Xr0 may need slightly over the nine months its had.
I am curious to know how you would handle tagged unions, say, something like this:
struct object {
int type; /* OBJ_INT, OBJ_STR, etc. */
union {
int i;
char *s; /* heap allocated */
/* etc */
} val;
};
How would you model things like reference counting? In CPython, for example, one of the most pernicious programming problems is invalid reference counting because the C API functions are rather inconsistent in their handling of reference counts. One has to carefully peruse the documentation to understand if the function will steal a reference (from a parameter), borrow a reference (for the return value), or if it makes a new reference. Such setups are perfect candidates for annotation.
As we explain in the article, Xr0's focus on formalising interfaces allows the verification of each function to be carried out independently. Thus we do reference counting only within individual functions.
I'm not sure I fully understand the CPython example. What I can say is that the annotations allow us to capture the semantics such as whether a function destroys a value, stores its value in a global or returned value, or has no net effect on the state of its caller.
Nobody is claiming this is the only possible way to make safe programs, as far as I know formal proofs a la seL4, when done correctly, can also prove the absence of essentially any kind of defect. The problem with multiple mutable references is that if you have them, you need some way to validate that across all possible mutable references to a given piece of memory, there are no unsafe concurrent accesses. Rust's claim to fame is "fearless concurrency", and as far as I know borrow checking with one mutable reference exclusive with all other references is the simplest approach to providing concrete data race safety in the face of still having mutable shared state across code. Nothing on this page even mentions data races, and I'm not sure how you would accomplish safety against data races from this design alone.
Most C programmers use C because they are forced to use it, by technical limitations like lack of compiler access or human limitations like lack of funding, curiosity or motivation.
C unfortunately became the API specification language of the most popular operating systems in the world. Both Unix and Windows world defines their low level system API using C types that strongly ties everybody and every program to C language, C standard library and the preferred compiler of the OS. Even Rust cannot escape it now. However Rust may give us hope / motivation and may force people to formally define the interfaces outside C so we can truly get rid of it one day.
Or other ecosystem effects; if I want to work on existing kernel code for pretty much any FOSS unix-family OS, C isn't possible to avoid, and AIUI even for all-new code it's still really spotty (like, you can write Linux drivers in Rust now, but only certain kinds of drivers).
I feel this frequently with C. I would love to formalize pointer use in interfaces. But Xr0's proposed syntax is clunky and not backward-compatible.
void foo(int* x) ~ [ free(x); ];
// <xr0.h>
#ifndef __XR0__
#define freed
#endif
// my code:
void foo(int* freed x);
As per the issue of backward-compatibility, Xr0 strips the annotations with a simple command: `0v -s`, producing C source that works with C compilers.
For complicated annotations, instead of
void foo(int* x) ~ [ free(x); ];
#include <xr0.h>
void foo(int* x) XR0( free(x); );
It also buys as the possibility of beauty. Shoehorning the annotations we're introducing into the preprocessor leads to constructions that aren't nice.
I think the problem with your example here is that it's a bit simplistic. In your example, if we drop the concept of ownership, sure it's not unsafe they can both point to the same allocation. But multiple mutable references can absolutely be a big issue. For example:
pub enum Thing {
AA(i32),
BB(String),
}
pub fn foo() {
let mut thing = Thing::BB(String::from("Hello"));
let Thing::BB(str_ref) = &mut thing else {unreachable!()};
bar(&mut thing);
println!("{str_ref}");
}
fn bar(_: &mut Thing) { ... };
This is literally the point we're making in the article. Note that what protects you from violating type safety is not the ownership rules, but the ability to propagate these rules by annotating `bar`. So we're proposing a direct focus on this propagation.
How anyone can think pointer arithmetic is elegant is beyond me. Especially when the title mentions a language with algebraic data types and higher order functions. Or even just RAII.
I'm also not sure C is the lingua franca of programming anymore. From my personal experience (and language is strongly tied to geography and culture) people tend to talk about strings and booleans, JSON and other custom types, stacks and heaps. ints and longs have fixed sizes and representations in their minds. (In fact, many C concepts are used erroneously from a strictly-C-language point of view.)
This is not to insult C, however, which is elegant in its simplicity (and perhaps The Mother of Modern Programming Languages, if you fancy a majestic title), nor the project, which has a noble goal.
> How anyone can think pointer arithmetic is elegant is beyond me. Especially when the title mentions a language with algebraic data types and higher order functions. Or even just RAII.
I have nothing against algebraic data types. They're great. With respect to elegance, I will refer to nothing more than this (from K&R):
/* strcmp: return <0 if s<t, 0 if s==t, >0 if s>t */
int strcmp(char *s, char *t)
{
for ( ; *s == *t; s++, t++)
if (*s == '\0')
return 0;
return *s - *t;
}
Yes. The ability to mutate an object necessarily implies the ability to mutate the state of an object to break guarantees. While there are definitely patterns where multiple mutable references to the same object can be safe, it is not inherently safe, and proving safety is far more challenging because you can't as easily rely on pre/postconditions for lemmas.
The particular case that makes the utility of a one-mutable-xor-many-read-only model clear is something I trip over surprisingly frequently in C/C++:
// Getting a value gets a pointer to somewhere in the hashtable...
Value &V = hash_table[key];
// This may cause the hash table to grow, thereby invalidating said pointer...
hash_table.insert(key2, value2);
// ... and now I used it!
V = meow;
Yeah, there are times when Rust's rule here pisses me off and feels too finicky, but it's also saved my butt several times. And quite frankly, a lot of the finicky can be worked around by building some solid container libraries to handle the cases where you can guarantee the safety with higher-level abstractions (say append-only data structures).
More to the crux of the article however, I'm not generally impressed with automated theorem proving as a solution to safety. Already from the meat of the article, it seems that this solution is setting you up for using a complex language to specify the interface, which immediately begs the question of how you can be sure the interface is correctly specified.
This is insightful. That is exactly what is happening, but our sense is that this language will be no more complicated than C itself, and will to a large extent parallel it.
The question is really what is more effective, working under one set of constraints imposed universally (like the ownership semantics in Rust), or taking upon yourself the responsibility of defining such constraints within each program. In this way what we're doing is an application of the "trust the programmer" design philosophy; trust him, not only to know what he's doing, but to be able to express it (in the interface specification).
> Sure, in a three-line function, it's kind of obvious (if you know to be aware of this possibility!), but in a function where the pointer and the use are separated by hundreds of lines of code, it's easy to miss that there is a requirement that the hash table not be resized between the two calls. With Rust, the fact that &mut for V means that I can't touch the hash table until I'm finished with V makes it a compiler error.
It can seem as though the example we provide is contrived (because of course it is), but it is not mere contrivance. The point we stress the most is not that the bug is obvious if there are only three lines, but that the presence or absence of a bug is impossible to see even with a single function call whose interface is informal. So what is remarkable is not that we can write three lines of code that have or do not have an obvious error, but that by the mere fact of the interfaces being informal, a three-lined function can be impossible to analyse by itself.
> The ability to mutate an object necessarily implies the ability to mutate the state of an object to break guarantees. While there are definitely patterns where multiple mutable references to the same object can be safe, it is not inherently safe, and proving safety is far more challenging because you can't as easily rely on pre/postconditions for lemmas.
This doesn't answer the question. "it is not inherently safe" does not mean "it is inherently unsafe", it only means "it may be unsafe". So our point is that Rust precludes many kinds of programming that can be safe in relevant contexts, and this is what is so limiting.
The point of interfaces is usually to hide underlying complexity. What's the point of interfaces that are just as complicated as their implementation?
> The question is really what is more effective, working under one set of constraints imposed universally (like the ownership semantics in Rust), or taking upon yourself the responsibility of defining such constraints within each program.
One of the things I personally like about Rust is that its rules are very simple and still capture 95% of all situations I find myself in. Adding the complexity of having to write your own formal specifications for the remaining 5% doesn't seem like it's worth the effort.
> So our point is that Rust precludes many kinds of programming that can be safe in relevant contexts, and this is what is so limiting.
Xr0 will also either 1) reject programs that are safe or 2) accept programs that are unsafe. An (computable) algorithm that decides for every C program whether it is safe or not is mathematically impossible. Start implementing loops and you'll quickly see why the idea of provable correctness without any restrictions is doomed to fail.
Not that similar projects don't exist: CBMC, Frama-C, ... How does Xr0 differ from those existing projects?
Specifications are typically less complex than implementations, so it won't be just as complex. One purpose of specifications is to encapsulate, but another purpose can be to specify a contract/protocol.
This is a pivotal question and our answer to it exposes one of our basic assumptions. Interfaces do hide underlying complexity, but that is not all that they do. They define our interaction with abstractions, which not only hide complexity, but reduce it by "abstracting". So what we find in practice is that the interfaces are not as complicated as the code, because all they define is what the higher levels of abstraction need to know to interact abstractly with the lower levels.
> One of the things I personally like about Rust is that its rules are very simple and still capture 95% of all situations I find myself in. Adding the complexity of having to write your own formal specifications for the remaining 5% doesn't seem like it's worth the effort.
Well this is great. If you like Rust, there's nothing wrong with that. But many C programmers don't feel this way.
> Xr0 will also either 1) reject programs that are safe or 2) accept programs that are unsafe. An (computable) algorithm that decides for every C program whether it is safe or not is mathematically impossible. Start implementing loops and you'll quickly see why the idea of provable correctness without any restrictions is doomed to fail.
Insightful again! This is all true. Note, however, that we aren't claiming not to impose restrictions. We're claiming that the restrictions should concentrate at a different place than where they concentrate in Rust. They should orbit around the interfaces. Xr0 is certainly imposing restrictions there.
Moreover, we are in no way suggesting/claiming that we can deduce the safety of arbitrary C programs, which is the whole reason the annotations are required. We're claiming that we can help programmers who already understand why their code is safe express these reasons in relatively-simple annotations, and use these to verify their reasoning.
Edit: typo.
Rust's restrictions can also be interpreted as restrictions on interfaces. A function taking (a non-`Copy` type) by value is a function that Xr0 would annotate as `free`ing that variable, for example.
> Moreover, we are in no way suggesting/claiming that we can deduce the safety of arbitrary C programs, which is the whole reason the annotations are required.
You are claiming that Xr0 will deduce that a function matches its annotations. If those annotations are "this function has property P", you'll have to deduce whether the function actually has property P. This can be augmented by inline annotations (i.e. annotations for code, not interfaces) and those will likely become necessary once you implement loops. But at that point you'll have reinvented Frama-C and you'll realize why Frama-C isn't used outside of safety-critical software: It's both hard and exhausting to use.
Yes they can, and we said this in the article, "The remarkable safety guarantees that Rust provides are consequent to something much deeper than its ownership rules: Rust empowers programmers to formalise and verify the semantics of pointer usage at the interface boundary between functions. If interface formality is the fundamental determinant of safety, systems language design should focus directly on it rather than on any other criterion, including ownership."
The point we're stressing, though, is that the restrictions in Rust do not focus on the interfaces, but on the ownership principle. So we're advocating for language design to ignore ownership considerations and deal with the interfaces as the important point.
> You are claiming that Xr0 will deduce that a function matches its annotations. If those annotations are "this function has property P", you'll have to deduce whether the function actually has property P. This can be augmented by inline annotations (i.e. annotations for code, not interfaces) and those will likely become necessary once you implement loops. But at that point you'll have reinvented Frama-C and you'll realize why Frama-C isn't used outside of safety-critical software: It's both hard and exhausting to use.
Again, I agree with most of this (except the cynicism). We have done some serious experiments with implementing loops and immediately saw that we would need to annotate the loops also (with at least some kind of invariants).
The comparison to Rust is actually a whole lot more helpful than that to Frama-C. Why is Rust able to deliver safety guarantees without becoming "hard and exhausting"? Our argument is that it is the interface formality issue that really determines safety. If this is so, why should it be "hard and exhausting" to be empowered with the ability to be formal at the interfaces concerning the things that influence safety?
The fact that we're using annotations does not mean that Xr0 is equivalent to Frama-C. To point to one important difference, we're focused on securing safety, whereas Frama-C is a general purpose tool for arbitrary correctness considerations. If Xr0 does grow to deal with such arbitrary correctness concerns, it is possible that it will become "hard and exhausting" like Frama-C, because of the inherent difficulty of complete verification. But while we're focused on safety alone, there's no reason why we can't offer something that is at most of the same difficulty level of working in Rust. Xr0's annotations are not "this function has property P" where P is arbitrary. They are "this function has well-defined behaviour according to the C standard under these circumstances". That is a much more limited kind of condition to validate.
Frama-C also does "interface formality". Chapter 3 (i.e. the first chapter after the one telling you how to install Frama-C) of the Frama-C WP tutorial is literally called "function contracts" and explains how to use ACSL to annotate pre- and post-conditions on functions.
> The comparison to Rust is actually a whole lot more helpful than that to Frama-C.
Your approach is way more similar to Frama-C than to Rust. The difference between Rust and Frama-C is that Frama-C allows you to specify arbitrary constraints, while Rust only allows you to specify very few and specific constraints. That may feel limiting (as you have pointed out) but that's also what makes it possible to deduce whether the function actually satisfies these constraints without having to annotate every loop (which is tedious for simple loops and hard for complex ones).
> If this is so, why should it be "hard and exhausting" to be empowered with the ability to be formal at the interfaces concerning the things that influence safety?
Annotating functions can be hard if the pre- or post-conditions of that function are hard to formalize (e.g. "this function returns the first element of a loop in the given linked list or null if no loop exists"), but having to annotate interfaces isn't what makes Frama-C hard to use. Frama-C is hard to use because it is hard to get it to accept that the function actually satisfies the function contract and this is a problem you will also face.
> To point to one important difference, we're focused on securing safety, whereas Frama-C is a general purpose tool for arbitrary correctness considerations. [...] They are "this function has well-defined behaviour according to the C standard under these circumstances". That is a much more limited kind of condition to validate.
Undefined behavior is extremely pervasive in C. If one of Xr0's goals is to verify that a C program does not exhibit undefined behavior (and it has to, given that undefined behavior is anything but safe) then you'll have to verify properties such as "this addition doesn't overflow", "this value is never INT_MIN", "this value is never negative", "this value is never zero", "a is less than b", ...
There will barely be any difference between verifying that a function has "well-defined behavior under these circumstances" and full verification.
let s1 = String::from("hello");
let s2 = s1;
println!("{}, world!", s1);
But yes, thread safety is down the road for us, when we get to C11.
We're beginning with what is central in C and then moving outward. C, as designed by Ritchie, and for the first 40 years of its existence had no official support for multithreading, so this can hardly be called central.
If we add support for multithreading it'll be after finishing with C89 and C99.
void with_bytes(size_t count, void (*cb)(void *bytes);
Programming in this style will force you to think about the life cycle of every allocation and there are ways you can still shoot yourself in the foot. But as long as you avoid storing references in static variables, you will generally avoid memory leaks and use after free when programming in this style.
And you can just do this with any c compiler without relying on new dependencies.
This seems to try to mimic Rust safety rails as impractical annotations. Even if these annotations can express non-trivial cases (which I doubt), they will constrain you for reasons Rust lifetimes can be constraining, you'll have to do tons of extra work, with crappy bare-bone programming language, inside an ecosystem where no one gives a crap and that can't even agree on a common sane tooling.
And then I have no idea from where does it follow that the at thend it will be "Safer than Rust".
How is that better idea than just using a most loved programming language along with a maturing large ecosystem that actually has a culture of building safe and reliable software, using approaches that are not bolted on but built-in?
int *p = malloc(1);
bar(p);
free(p);
Excepting that, why are you annotating functions, it's the pointer itself that has the use case invariant. Shouldn't the type be annotated to declare these semantics instead?
> Wouldn't the safe way to write that code be to just allocate the value on the stack so it has automatic lifetime managed for you?
To be fair, there are a lot of reasons why you might not do that. One reason is that stack space is limited, so if you are allocating a large object, it would be unwise to necessarily use stack space in some cases, as you might overflow the stack, and it's hard to know if your code is overflow-prone since different platforms have different default max stack sizes. Another reason is if you don't know how much memory you might need at compile-time and thus can't use static allocations. Finally, and probably one of the main reasons, sometimes the lifetime of a memory allocation just doesn't map to a stack frame; it may malloc/free within one stack frame, or it may malloc and then get freed in a parent stack frame indeterminately. Basically, any reason you might use a smart pointer in C++ is also a reason you'd reach for dynamic allocations in C.
Sure, if you malloc(1) specifically, you know it's only one byte, and a static allocation. But clearly, that's just a contrived example, so focusing too hard on it is a little silly.
> Excepting that, why are you annotating functions, it's the pointer itself that has the use case invariant. Shouldn't the type be annotated to declare these semantics instead?
Their entire hypothesis is the idea that the boundaries between interfaces is where the unsafety occurs. The pointer itself has the invariant, but locally proving invariants like "pointer can never be freed twice" or "pointer is either freed or returned" can be done trivially using control flow analysis; the problem comes when you start calling other functions. If you add annotations and make it a compiler error to have invalid annotations, you can make it so that these invariants can extend across function boundaries without needing to recursively prove the control flow over the entire program, which would usually be infeasible due to the amount of possible code paths.
I'm not suggesting this is necessarily the best way to go FWIW, but this is also pretty similar to how, say, TypeScript adds incremental safety to JavaScript; null safety is accomplished by having not just the types but also the interface boundaries contain assertions that can be checked on both sides to avoid needing deep, recursive control flow analysis.
I would prefer something like this:
void* foo() /* return malloc(SIZE) */ {
void *p = (void*) = malloc(SIZE);
bzero(p, SIZE);
return p;
}