This is one way to go; but the only "problem" with C is management's expectation that production software can be written by people who have only half learned the language, and that is a problem irrespective of which language we are talking about.
I think this is actually one of the selling points of C over other languages. Certainly it's easy to fool yourself into thinking you know any language better than you do, but C genuinely is relatively tiny, and I think it's reasonable to expect to become familiar with almost everything in the language in a month or so of full-time work. After a decade of day job C++ coding, I'd not say the same for myself there.
Rust and C++ lately have been particularly quickly moving targets to keep up with, where C is still pretty much the same as C99. The compilers are better, their warnings are better, sanitizer modes are incredible, but the things you type into your text editor to express your program structure are still pretty much the same thing.
Not really that much In my experience. Most of the unsafety is very obvious and most of the memory safety really come from errors from this obviously unsafe parts, e.g. the most common memory safety bug is pointer arithmetic gone wrong. The others are temporal memory safety and signed integer overflows. None of this is really subtle or what I would really call a footgun. Nowadays, programmers do not seem to understand integer conversion rules of C anymore (although they are simply IMHO), but then this is something which can be mitigated via sanitizers.
I could have been more precise when I said it's easy to fool yourself into thinking you know _any_ language better than you do... both rustc and ghc have made it abundantly and repeatedly clear that I don't know Rust and Haskell well, and the "if it compiles, it's probably correct" trust that develops from that frustration is a great asset to both those languages.
But those are exceptions: I've definitely felt like I've known more than I really did about at least C, C++, Java, Scheme, Python, Go, bash, Javascript, cron, and several assembly variants, and those platforms did little to stop me from learning about my inexperience in difficult, sometimes embarrassing, sometimes expensive ways.
I'm a big fan of more compile time analysis any way it can be done, and whatever can't at runtime. More types, more proofs, more fuzzing, more sanitizers, and also where possible, more restricted execution models than Turing-complete. Any code that can't prove itself correct is a serious liability. I just also like C... it's got many footguns, yes indeed, it's practically constructed out of only footguns, but there are only like 8 of them, and they're all right there waiting for you to get to know them. It's like having a few good sharp knives in your kitchen. You get to know each well, using them one at a time---and if any is missing from the block you pause everything and look around very carefully.
I doubt that a month of so of full work will get someone fully proficient on e.g. the finer details of integer promotions and how they can break things in non-obvious ways (think of situations such as combining signed and unsigned operands of different widths). The fundamental problem is that sane production code written in C will generally deliberately avoid some aspects of the language precisely because they are so footgun-prone, which means that if you learn solely by experience, you may never even become aware of the footgun behind the pattern.
I think one of the problems with C today, which you're touching on but I think not quite capturing, is that it's not taught and used nearly as much anymore. So when people are found in the position of writing, or more likely altering existing C, they usually don't know popular styles, conventions, coping mechanisms; eg. you can use coding style to make memory leaks less likely [one example: a rule forbidding early return out of a function, designating cleanup blocks], but few people are learning or teaching it.
I fully agree than most of problems of C can be mitigated with good training. It it of course far easier to blame the language than admit that there is a skill issue. The story that this a language full of footguns that even experienced programmers can not deal with is a lot of nonsense in my opinion and does not match my experience (both as a C programmer, a manager of C programmers, and user of many rock-solid C programs). At the same time, does it help to complain about insufficient training? It is just reality that many programmers are not experienced in C and it is also true that there are a lot of serious problems in C code. This is not a contradiction. If you have C coders without sufficient training and/or experience you will get memory safety issues in C code and you will not even notice in time. If you have unexperienced Rust coders, you will still get memory safe code - at least if you have a rule against using "unsafe" or some oversight. (the code might be buggy in others ways, or programmers may be less efficient, but you still get memory safety ensured by the language). I think this is the real great advantage that Rust has and why we should also have a memory-safe subset of C.
I don't think knowledge of the language is the issue with C, it's the fact that it requires a huge amount of diligence to not have security issues. Knowing the nooks and crannies of the language doesn't really help with that.
Made worse by the fact that most people don't work with it or get taught it as much as 25 years ago. A dev who has come up in the last decade or more, the typical C experience they have is writing it poorly for college. They're not typically battle-hardened on it, few people learn the best practices anymore. But when existing code doesn't suit a need they still might be tasked with maintaining something or fixing bugs.
Outside of tiny languages though, pretty much nobody knows the "whole" language. Almost every production language has a ton of quirks that can surprise people who have been using a language for years.
And frankly large numbers of features in languages aren't needed by most devs. Marshalling in C#, for example, isn't needed unless you're calling into native code. Making raw syscalls in Rust isn't needed unless you're working on optimizing some low level systems code.
Expression trees in C# is also an example of this.
I have 10+ years experience (and consider myself highly proficient) in C#, but my interaction with expression trees is mere hours where I've only once or twice needed to solve a very specific small problem which I could do with a small tweak to code copied from Stack Overflow.
I don't think it is the only problem. Even if you learn the language and know it well, if you start contributing on a big project, it's going to be hard to understand exactly what happens and to be sure that you didn't make mistakes. At this point it makes sense to delegate some checking to the computer.
>the only "problem" with C is management's expectation that production software can be written by people who have only half learned the language, and that is a problem irrespective of which language we are talking about.
Obviously that's not "the only problem", else there wouldn't be huge style guides forbidding tons of practices to make programs safe for NASA and other such uses, aimed at the expert C programmers hired there.
Also obviously that is not "a problem irrespective of which language we are talking about", unless half-knowing the language has the same impact and the language have the same footguns, which is nowhere near true for other languages versus C. You can "half know" Java and not ever get a buffer overflow. You can know C quite well and still get all kinds of dangerous bugs into the code.
It's not usually that someone only half knows the language but rather that different people in a team can carry different assumptions about how something was done...
it takes literal years for someone to get to a point where they can ship proper c code and the process of getting good requires shipping c code when you don't know everything yet. having a system that automates and enforces years of collective knowledge on juniors is great and lets them contribute while they acquire experience.
Are any of the many "safe versions of C" getting any traction? There have been so many. It's not a technical problem. It's a mindshare problem.
The future in this area may be something that takes in existing C code and uses a LLM to recognize idioms and annotate. Without some automated way to convert legacy code, this isn't going to happen.
(One big problem with converting to Rust is that Rust's data model is so far from C/C++ that you can't really convert much existing code. You have to rethink the design to fit the affine type model. That's hard.)
Right now I'm ~90% through a major rewrite to use GC instead of isoheaps, because then I'll go from rewrite-a-bit (Fil-C previously required malloc calls to be annotated and for some unions to be changed) to rewrite-nothing (malloc will Just Work and so will unions).
I hope there are others also trying various alternatives. It's too soon for most of these things to tell what traction they may or may not get.
Rust's data model diverged from C++, but it's not very far from C. It's easy enough to write C-compatible structs and functions in Rust, as long as you don't need `Drop`. Even tagged unions (data carrying enums) are supported to some degree.
It's the lack of backlinks to parents that gets you. Rust can do hierarchies where an A owns a B which owns a C, but if you have a reference to C, you can't get back to A. (Yes, weak pointers, reference counts, unsafe hacks, etc. can work around that. But the language really doesn't like links to parents.)
So there's no direct translation from a C++ object hierarchy to Rust structs.
> (One big problem with converting to Rust is that Rust's data model is so far from C/C++ that you can't really convert much existing code. You have to rethink the design to fit the affine type model. That's hard.)
True, but that's likely going to be the case as well to convert to any ”safe version of C” as well, because in the general case the safety of a C program is undecidable: to make it safe, you have to restrict it to a subset of behaviors that can be statically proven as safe, and the borrow checker and “Rust's data model” is just that.
You have to understand the code at a level sufficient to make accurate annotations, which isn't that much easier. And you're not getting as much safety bang for your buck for the effort as you would in a rewrite in actually safe language.
> You have to understand the code at a level sufficient to make accurate annotations, which isn't that much easier
That's not necessarily true though.
Half decent C code already has a coherent memory management strategy. The problem is that humans can't follow even pretty straight-forward memory management strategies 100% of the time. If you have a function that returns memory the caller is required to free, or accepts a parameter that the function takes ownership of, that can be easily expressed but hard to get right every time.
In fact, functions typically document this... in half-decent C code. So we're really talking about formalizing the expression of memory management documentation that already exists and is already understood.
> And you're not getting as much safety bang for your buck for the effort as you would in a rewrite in actually safe language.
I just can't think of what the rational argument for this could be. A complete deep rewrite -- where the new language requires reorganizing the code at a low level so that a lot of existing logic cannot be reused (as-is, or transformed in certain specific ways) -- is extremely costly. It is on the order of the total cost of writing the software in the first place plus the entire cost already spent maintaining it over time. Some costs -- like the goodwill of users/adpoters -- simply cannot be paid again at the same rate. For large scale software there would be numerous regressions over a long period of time, while at the same time the software stops adding many new features, since all the focus will on the rewrite and bugs related to the rewrite. I will stand corrected if there is more than one or two exceptional cases of large scale software making a successful transition of this sort without paying a massive cost.
If you don’t understand the code well enough to annotate it, it seems hard to believe you’d able to rewrite it and end up with the same functionality (same processing rules, accepts identical input, produces identical output, etc).
You certainly could get the same level of safety via annotations as you can in safe language. And if you transition existing code, you do not need to rewrite that will introduce new bugs and invalidate all the testing.
>> understand the code at a level sufficient to make accurate annotations, which isn't that much easier. And you're not getting as much safety bang for your buck for the effort as you would in a rewrite in
But rewriting assumes I learn a new language on top of rewriting.
It's still better than a complete rewrite, which will very likely introduce new bugs that had already been fixed in the existing code (no matter what languages are used).
As someone who tried to get Frama-C working on existing code: No, annotating existing code is not much easier than rewriting it. In fact, to make these annotations practical, I had to rewrite parts of the code anyway.
That just means you need a whatever-to-C transpiler. Which in most cases is quite achievable, and especially so if the language is designed to allow that (so e.g. no guaranteed tail call optimizations etc).
It could be helpful if the annotation can be stripped out if needed for use with older compilers (especially important for older microprocessors that won't ever have it's C compiler ported).
Less ceremony than Rust (and no ball-breaking fighting the borrow checker), a lot faster than Go, way more mature than Zig, and with more immediate compatibility with tons of code, more support, more developers, and more mature compilers than any of the above.
The problem with black-and-white thinking is that it's too simplistic to apply to the great majority of real-world problems.
Safe C provides an incremental migration path from unsafe C to safe C. And you don't need to completely rewrite, but instead address the issues flagged, which will often be a lot less work and risk than an actual rewrite in a new language. (This seems obvious to me, but apparently not?)
This is our thinking as well, a complete rewrite in another language (short of formally verifying the code) could introduce all sorts of logical bugs that did not exist or were patched in the old code.
You wouldn't - you'd write it in the safe C subset?
Presumably it's easier to rewrite part of your app rather than the whole thing.
But I'm all for a safe version of C17 (or C23/24). It's so disappointing that there isn't a standard memory-safe compiler/runtime/ABI. (And while they're at it, the stack should grow up rather than down.)
Perhaps CHERI or similar will catch on someday. Maybe Apple could try implementing memory checking for clang and Apple Silicon.
I am currently working on a GCC frontend that has a memory safe mode where it would warn about every unsafe constructs. At the same time a trying on modifying some of my projects to work with it. To me, this seems an entirely reasonable approach. But it is a spare time project, so progressing slowly.
Annotating, possibly incrementally, existing code would be way easier than a rewrite.
Safety annotations is the directions that C++ has been attempting without much success for a while though, so I'm not very optimistic. But I'm always happy to see another attempt.
C has a minimal, interpreted, safe, functional language embeded into it. You just have to execute it with cc -P -E, no need to run any fancy generated binary.
Homepage seems to focus mostly on temporal memory safety; there isn't much said about spatial memory safety or memory-safe-but-unsound primitives, like type confusion.
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.)
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.
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.
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.
We chose to start with temporal safety (use-after-free, uninitialised memroy etc) but are going to implement spacial safety (buffer overflows/underflows) soon (See roadmap https://xr0.dev/vision-roadmap).
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.
C doesn’t particularly strong safety guarantees of its own around type punning, which is logic bugs that aren’t themselves memory corruption so frequently result in exploitable vulnerabilities in C (and C++) codebases. How do you plan to handle things like that?
(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!)
They need a guide to compare it frama-c and other systems with annotations. Or at least compare what the objective ultimately will be, since this is still in its infancy.
Yeah, this doesn't really do anything for now. It currently doesn't even implement loops.
I don't see why I would ever choose this over Frama-C which basically does the same (and is actually battle-tested). I just don't see a niche:
- No full control over runtime needed: Java, C#, Python, ...
- Full control over runtime and memory safety: Rust
- Full control over runtime, memory safety and provable absence/presence of certain behaviors (i.e. aerospace, nuclear reactors, ...): Frama-C, CBMC, Astree, ...
Where does Xr0 fit in and how does it differ from existing technology? The fact that they don't even mention any of those tools makes me believe that they are either not aware of them or that they are aware and the difference between this and Frama-C is just syntactic. Not a good look either way.
Since we are not academics, I don't see why we're under obligation to do a comprehensive literature review, especially early on. We aren't claiming to have invented these techniques. It should be obvious that Xr0 involves very little in the way of new ideas. Our primary reference has been the work of Dijkstra.
What is significant about Xr0 is how it applies these old ideas. Xr0 is designed for programmers rather than mathematicians, so to us syntax matters a great, great deal.
> Since we are not academics, I don't see why we're under obligation to do a comprehensive literature review, especially early on.
I don't think you're under any obligation, I just think that not discussing prior art is a bad look.
> What is significant about Xr0 is how it applies these old ideas.
I don't see anything new about the application of these well-known ideas either. Especially nothing that could explain why Xr0 would be widely used, while Frama-C is extremely niche.
> Xr0 is designed for programmers rather than mathematicians, so to us syntax matters a great, great deal.
Proving (the correctness of code) is an inherently mathematical task. So if by "mathematician" you mean someone who does mathematics, then all of your users will be mathematicians.
> I don't think you're under any obligation, I just think that not discussing prior art is a bad look.
See [0] where our reliance on Dijkstra is transparent.
> I don't see anything new about the application of these well-known ideas either. Especially nothing that could explain why Xr0 would be widely used, while Frama-C is extremely niche.
Begin with the fact that Xr0 is written in C and feels like C. We're building it so that C programmers will be able to use it without explicitly learning about formal verification.
> Proving (the correctness of code) is an inherently mathematical task. So if by "mathematician" you mean someone who does mathematics, then all of your users will be mathematicians.
Absolutely true. But what I mean by "mathematician" is a self-conscious mathematician, or at least someone with a background in formal mathematics.
> See [0] where our reliance on Dijkstra is transparent.
Mentioning that you're vaguely inspired by Dijkstra is not the same as discussing prior art. And it's not like there isn't enough prior art about "safe C" out there [0, 1, 2, 3, 4, 5, 6, 7, 8, 9].
> Begin with the fact that Xr0 is written in C and feels like C. We're building it so that C programmers will be able to use it without explicitly learning about formal verification.
Most of the people interested in formally verifying their C code will already know about formal verification and absolutely don't care about whether Xr0 is written in C or not.
> But what I mean by "mathematician" is a self-conscious mathematician, or at least someone with a background in formal mathematics.
I'm doubtful Xr0 will be useful for someone without a background in formal verification.
To me, the whole project seems like vapourware. It currently works on an extremely limited subset of C. In fact, this subset is so limited that from a computation theory standpoint, the current capabilities of Xr0 are trivial. Supporting while loops (or general recursion) on the other hand is impossible (from a computation theory standpoint).
Even on this small subset of C it took me five minutes to get an out of memory error and a further five minutes to craft a C program with a double free that passes verification [10].
All this combined with a website that makes great promises about how awesome Xr0 is (or rather going to be) and handwavy explanations about how easy adding the missing features will be that don't hold up to any scrutiny. Dozens of similar projects exist, few of them work at all on non-trivial C programs and all of them require herculean effort (and are thus only used for safety critical software) to correctly annotate C code (often this includes rewriting parts of the code to make the annotations simpler or unnecessary). There is no discussion at all how Xr0 is going to solve the problems that killed these projects.
> Even on this small subset of C it took me five minutes to get an out of memory error and a further five minutes to craft a C program with a double free that passes verification [10].
Nice work with the program. However, the only reason it verifies is we haven't yet implemented `||`, so in the parser the phrase `if (x || !y)` is being interpreted as `if (x)` (see [0] for the relevant production). This may seem like another frustrating indiction of how "extremely limited" the subset of C that Xr0 works on is, and indeed it is. But the most important point is there is no logical flaw in Xr0's design here, and no reason whatever that an error of this kind wouldn't be detected. [1] is an equivalent program that shows the logical cogency of our approach (I know it's ugly!).
> I'm doubtful Xr0 will be useful for someone without a background in formal verification.
> Most of the people interested in formally verifying their C code will already know about formal verification and absolutely don't care about whether Xr0 is written in C or not.
We aren't making Xr0 for people (self-consciously) interested in formal verification, but for C programmers interested in safety of the kind that Rust provides. And I can tell you that C programmers prefer their tools in C.
> All this combined with a website that makes great promises about how awesome Xr0 is (or rather going to be) and handwavy explanations about how easy adding the missing features will be that don't hold up to any scrutiny. Dozens of similar projects exist, few of them work at all on non-trivial C programs and all of them require herculean effort (and are thus only used for safety critical software) to correctly annotate C code (often this includes rewriting parts of the code to make the annotations simpler or unnecessary). There is no discussion at all how Xr0 is going to solve the problems that killed these projects.
Fair enough. The proof is in the pudding. Give us a few months. But understand that we have limited resources (this is an open source project and we're working on it part-time). We could either stop and make long-form arguments with full bibliographies or focus on building Xr0 into what we say it's going to be.
> However, the only reason it verifies is we haven't yet implemented `||`
You should error on constructs you don't yet support. Not doing so makes it very difficult to ascertain how well Xr0 works.
> We could either stop and make long-form arguments with full bibliographies or focus on building Xr0 into what we say it's going to be.
You didn't do either though. You wrote long-form arguments about how awesome Xr0 is (or going to be) and how groundbreaking the idea of "interface formality" is. If instead you actually produced a working prototype (or even any technical argument why such a prototype is feasible) I'd be way less doubtful.
> You should error on constructs you don't yet support. Not doing so makes it very difficult to ascertain how well Xr0 works.
You're right. We should. (We will be adding this as we are able.)
> You didn't do either though. You wrote long-form arguments about how awesome Xr0 is (or going to be) and how groundbreaking the idea of "interface formality" is. If instead you actually produced a working prototype (or even any technical argument why such a prototype is feasible) I'd be way less doubtful.
A 7-point blog post is hardly "long-form" :)
But more to the point, Rust has already achieved this "interface formality", as we state in the second paragraph of this "long-form" piece. That achievement on the part of Rust is indeed groundbreaking. Is it so crazy to claim that this can be replicated for C, without encumbering it with ownership considerations that have no relationship to interface formality?
Fair enough. We have a much more generous definition of "working prototype" than you do. Hopefully one day soon we'll have something that clears yours.
> Is it so crazy to claim that this can be replicated for C, without encumbering it with ownership considerations that have no relationship to interface formality?
You're not replicating what Rust does, you're replicating what Frama-C does.
Then again, even just replicating what Rust does would be extremely difficult (if not impossible) given the pervasiveness of undefined behavior in C.
> Fair enough. We have a much more generous definition of "working prototype" than you do.
How many useful C programs do you know that require no loops and no binary operators?
> The purpose of the prototype is to show the feasibility of the approach we've taken
But it doesn't do that. You haven't shown that this approach is able to deal with loops and loops are pretty fundamental to every C program.
Heck, you haven't technically shown that this approach can deal with binary operators. I would love to turn Xr0 into an improptu SAT solver, but without `&&` and `||` that sadly isn't possible right now.
Then why not write a blog post "We can parse C" instead of "Xr0 makes C safe (it doesn't actually and we are unable or unwilling to go into details and also please don't ask us about Frama-C)"?
Avoiding UB in single threaded programs is the easy part. It's harder for a low level language like C, but not too hard.
But avoiding UB in multithreaded programs is very very hard. Many "safe" managed languages have UB when you misuse synchronization mechanisms, like Go.
Some languages Java and OCaml manage to avoid UB when you have data races. They do so by disallowing some compiler optimizations. OCaml is the better one in this regard (see the paper "bounding data races in time and space")
It is the best written reply in this thread. The style is great, up until "ur azz". I'd have appreciated a less hackneyed metaphor, but I can understand the author wanted to finish the lament.
What does surprise is me why someone is so strongly opposed to something that is optional, is a support, and doesn't even get in the way of laying bare the algorithm. It's an annotation to the function declaration, not unlike a return type. Perhaps it's the verbosity?
Quite frankly, the "leave me alone, I know what I'm doing!!1!" people have had over 50 years now to prove that they can consistently write safe code as a group. All evidence so far points to the contrary.
FWIW I don't think Rust is the answer to this, either. Most software just needs to be written on an even higher abstraction level, with copious redundant safety nets embedded on all levels, performance be damned. It appears that that's the only way we as an industry can reach acceptable quality of software with the average developer that we actually have (as opposed to the hypothetical Zen master).
This is another good spot. Xr0's logical/arithmetic analysis is currently limited because we've been more focused on getting the structures of the language working as a whole. So you'll get more of these asserts if you try using `&&`, ternaries, and so on.
void x(int a, int b) {
int * p;
p = malloc(1);
if(a) {
free(p);
}
if(b) {
free(p);
}
}
It is possible that the program always guarantees that a!=b, but it would be hard to prove even with whole program analysis. Are you planning additional annotations or this is just not expected to work?
I can't speak for the authors but I think I'd file that one under "and if you write this, ideally a small gnome exits the back of the computer and hits the developer with a mallet."
I'd be perfectly happy refactoring that so I could have an 'a or b' test (I'm assuming $something means that x(0, 0) not free-ing is correct in real code because nitpicking an illustrative example would be silly).
Though note that I'm sufficiently bad at tracking things right when writing C that I tend to spend most of my debugging time figuring out what stupid mistake I made to cause the current segfault - so I'm probably more willing than average to write code differently if it helps me avoid that ;)
This is another good find. We haven't yet implemented the `!=` operator (or most of the binary operators).
Incidentally, you will notice that Xr0 rejects the program as is, which is correct (because of the double free).
It can, however, accept code like the following:
void
foo(int a, int b)
{
int *p;
p = malloc(1);
if (a) {
if (!b) {
free(p);
}
}
if (b) {
free(p);
}
if (!a) {
if (!b) {
free(p);
}
}
}
I say "can" because we only have this working on a development branch [0], and there are still some issues we're resolving on this, hopefully by next week.
Ideally you would express the precondition that a and b are mutually exclusive like this:
void x(int a, int b) {
if(! (a != b))
abort();
int * p;
p = malloc(1);
if(a) {
free(p);
}
if(b) {
free(p);
}
}
And the program would be accepted. I'm on my phone and can't verify it though.
Great stuff anyway!
Edit: is the algorithm documented anyway? And there is any reason why you guys are not implementing it as a clang/GCC plugin and using the new C and C++ annotation syntax?
Yes, the code example you've given is exactly in the direction we're thinking. (Edit: thought it can't be verified yet.)
We haven't documented the algorithm because it's not the unique part of what we're doing. It works in a very simple-minded way, analysing possible states.
The interesting part is the insight that function interfaces are the boundary along which verification should take place. Applying this idea consistently we escape the combinatorial explosion which tends to plague efforts in this area, because every function can be verified by itself. Notably, Dafny recognised this point before us, and the earliest clear statement we can find regarding it is in Dijkstra's "Notes on Structured Programming", in his chapter "On a Program Model". You may find that illuminating read.
I'm no expert on Clang/GCC and the new annotation syntax for C and C++, but from what I've seen it's not general enough for what we're trying to achieve in Xr0. The safety semantics which are expressed in annotations in Xr0 (see [0] for an example) get very detailed.
Will take a look at your reference. Stroustup and Sutter have tried annotating every function, but their declarative function wasn't expressive enough. Adding arbitrarily expressions might help though.
Re annotations, I meant the attribute syntax. You can have arbitrary custom syntax in it:
Plus, at -O1 and up, gcc optimizes this away, so the check itself is not well-defined as necessary.
Does it always make sense to strictly enforce code that will be optimized/changed during compilation? Or does Xr0 run after compilation/linking?
How to handle things like unions where you want data in a nice mixed-type struct that is used locally and can also be sent as a stream of uint8_t over a wireless connection? Then, the last function that needs to use the memory frees it. Or is that still fine as long as you malloc once somewhere, free once somewhere, and annotate that the memory region will be accessed as more than one dereferenced type?
Much more important: Will the proposed changes be understandable enough for your average CS undergrad to learn in four months of halfway diligent study? (Then again, you might do away with students taking time to debug improper malloc/free and whatever else falls under the scope of Xr0...)
I loved it. It gave you much (not all) of that "if it compiles it works" good vibes that Rust has. Though, oh boy, were you in for a surprise if you think that Rust compiles slowly. You could probably do something similar with C:
DbC is awesome because it formalizes what conditions must exist before and after a piece of code runs and defines who (caller vs. callee) is responsible for what parts.
There are earlier attempts to do this, CCured was as I recall wholly based on comment annotation, and it was also closely related to cyclone, which inspired rust.
Have you looked at them? Always good to look at prior art, it's not easy what you're trying to do.
Pretty sure I still have the CCured code lying around in a backup somewhere, I downloaded it and played with it long ago. If it's truly not available on the net anywhere, I suppose I can try to dig it up.
Do you think C has a better syntax compared to Rust? I'm honestly not sure about this. It surely heavily depends on your preferences, though. Generally speaking, what do you think?
It has a generally simpler syntax, except for function pointers and arrays, but I wouldn't call it "better". Comparing syntaxes of such different languages is pointless anyway. Syntax should serve semantics.
"Simpler" is the word that we care about. Although Rust is an advance on C in many significant ways, what it loses is the simplicity. One of our goals is to offer three same advances (and more) but without compromising on simplicity.
If 0v can tell what the abstract needs to be, why do we need to write it down? It has to know the abstract to compare against the annotation. Maybe it's so we better understand the origin of the problem, rather than getting 'free error' at the end of a long chain of functions?
It also can't in general deduce whether the abstract and the implementation match, as doing so would require solving the equivalence problem (which is undecidable for anything as or more powerful than pushdown automata).
I'm not very familiar with the equivalence problem, but at least for Xr0 abstracts (what we call the annotations attached to functions & loops) there is an extremely strong structural similarity between the implementation and the annotation. So it's not at all clear that we'll run into this.
> If the annotation is basically just a copy of the function body why have any annotation at all?
This is a profound question. Xr0 annotations seem to be copies of the function bodies, but they aren't actually. What they are is a description of the function's safety semantics, the side effects and circumstances under which the function may be relied upon to exhibit well-defined behaviour (under the C Standard).
They only seem to be copies of the bodies because we're dealing with simple examples in the post here and in the tutorial, but we have a much more significant program ready (documenting) that we'll be sharing soon that shows the difference more clearly.
Xr0 is built in explicit reliance upon the powers of programmers to structure code in such a way that the annotations become simpler and simpler as you move up layers of function abstraction. As a simple example, think about what happens when you allocate memory and free it within a function, e.g.
Note that `foo`'s annotation is like a copy of its body, but `bar`'s annotation is very simple, even though it interacts with `foo`, which is only safe if the pointer it returns is handled. So from `baz`'s perspective there are no safety semantics it has to worry about when it interacts with `bar`. The complexity that could lead to safety bugs in `foo` has been completely handled in `bar`.
We call this simplifying phenomenon denouement, and well-designed programs exhibit it very strongly. Our belief that programmers can design constructs that tend towards denouement as one moves down the call stack towards `main` is one of the basic reasons we're working on Xr0.
> It might not be clear to you, but if you want to allow any annotation with the same semantics as the body of the function you will run into this.
Yes, but we don't. Only well-defined behaviour according to the C Standard. This is the goal for Xr0 v1.0.0. After that the sky is the limit.
> Xr0 annotations seem to be copies of the function bodies, but they aren't actually.
You're constantly dodging the question. If annotations aren't copies of function bodies (which is really the only sensible choice), you need to deduce whether a function body matches the annotations. "Structural similarity" between C and your annotation syntax won't make this easier. In fact, it is impossible to deduce whether two C functions are semantically equivalent even though C is extremely structurally similar to C (you could even argue that C and C are structurally identical).
> Our belief that programmers can design constructs that tend towards denouement as one moves down the call stack towards `main` is one of the basic reasons we're working on Xr0.
So your main criticisms of Rust will mostly also apply to Xr0: You need to rewrite existing C code to make annotations practical (and at that point you might as well reimplement it in Rust) and Xr0 will limit the constructs you will use in your code, because annotations will be impractical for code that isn't written for "denouement".
> If annotations aren't copies of function bodies (which is really the only sensible choice), you need to deduce whether a function body matches the annotations. "Structural similarity" between C and your annotation syntax won't make this easier. In fact, it is impossible to deduce whether two C functions are semantically equivalent even though C is extremely structurally similar to C (you could even argue that C and C are structurally identical).
Maybe I don't understand your point. I am not denying that we're deducing that the body matches the annotations. I'm simply saying that for the restricted case of safety semantics alone, this deduction can be done. Yes, it is impossible to deduce semantic equivalence of arbitrary functions. The question is whether it is possible to deduce that annotations capture the safety semantics of the body. If you have a concrete example it would be helpful here – but for the restricted concerns of safety, not for arbitrary constructs.
> So your main criticisms of Rust will mostly also apply to Xr0: You need to rewrite existing C code to make annotations practical (and at that point you might as well reimplement it in Rust) and Xr0 will limit the constructs you will use in your code, because annotations will be impractical for code that isn't written for "denouement".
Your quote omits the first sentence of the paragraph, which states that "well-designed programs exhibit [denouement] very strongly". Denouement in the sense we're referring to is an absolute theoretical necessity for any safe program, because at some level (of functional abstraction) the safety concerns must be handled, otherwise the program would have a safety vulnerability.
Xr0 definitely limits constructs, but our claim is that the limitation we're imposing is one that reflects the structure of all safe programs. The same cannot be said about Rust's ownership semantics, which limit an enormous number of simple, safe constructs. So the C programs to which one would be adding Xr0 annotations wouldn't need to be rewritten unless a bug has been discovered.
> I'm simply saying that for the restricted case of safety semantics alone, this deduction can be done.
And I'm saying it can't be done, at least not in a fundamentally less tedious and hard way than Frama-C.
> Yes, it is impossible to deduce semantic equivalence of arbitrary functions. The question is whether it is possible to deduce that annotations capture the safety semantics of the body.
It isn't in general.
> If you have a concrete example it would be helpful here – but for the restricted concerns of safety, not for arbitrary constructs.
Safety is not a "restricted concern": You can for every property P easily construct a function that is safe if and only if property P holds. I'll be using Python because this example (which I like) requires arbitrary size integers. You could obviously also implement this in C, you'd just need to implement arbitrary size integers (or use a library that implements them):
def collatz(x):
if x % 2 == 0:
return x // 2
return x * 3 + 1
def cycle(f, x):
tortoise = f(x)
hare = f(f(x))
while tortoise != hare:
tortoise = f(tortoise)
hare = f(f(hare))
return hare
buffer = [0, 0, 0, 0, 0]
x = int(input())
if x >= 1:
collatz_cycle_element = cycle(collatz, x)
print(buffer[collatz_cycle_element]) # this is safe (or is it?)
This takes as an input an arbitrary positive integer x, searches for a cycle in the Collatz sequence beginning with that number and returns an arbitrary element of that cycle. It is conjectured that for every positive integer this cycle will be 4 -> 2 -> 1 -> 4 -> ... and thus this program is safe if and only if the Collatz conjecture holds.
Another example would be a C program that generates random planar graphs, computes their chromatic numbers and then collects statistics about them in an `int statistics[5]`:
#include <stdio.h>
void main() {
int statistics[5] = {0};
for(int i = 0; i < 1000; i++) {
struct graph g = generate_random_planar_graph();
int chromatic_number = compute_chromatic_number(g);
statistics[chromatic_number] += 1;
}
printf("%i, %i, %i, %i", statistics[1], statistics[2], statistics[3], statistics[4]);
}
The safety of this program requires you to prove that `generate_random_planar_graph` always returns a planar graph, that `compute_chromatic_number` correctly identifies the chromatic number and that the chromatic number of every planar graph is less than 5.
Thought provoking stuff! I really appreciate how much effort you've put into this.
However, the main reason why this argument is flawed is it omits the heart of the matter: the annotations. Xr0 empowers programmers to propagate safety semantics. A program that is only safe if the Collatz conjecture holds is (surprise) only safe if the Collatz conjecture holds. So in Xr0 the only requirement we would impose is that this program be augmented with an annotation that communicates that it is only safe if the Collatz conjecture is true.
So the flaw in the reasoning is we haven't claimed that Xr0 can prove arbitrary programs are safe. We've claimed that Xr0 can prove the correspondence between the safety semantics denoted in an annotation and a function body. Above there are no annotations given which would specify "this program is safe only if the Collatz conjecture is true". It shouldn't be hard to prove the correspondence between such an annotation and the program you've written, e.g.:
def main(): ~ [
buffer = [0, 0, 0, 0, 0]
x = int(input())
if x >= 1:
collatz_cycle_element = cycle(collatz, x)
print(buffer[collatz_cycle_element])
]
buffer = [0, 0, 0, 0, 0]
x = int(input())
if x >= 1:
collatz_cycle_element = cycle(collatz, x)
print(buffer[collatz_cycle_element])
It's the principle of propagating the safety-determining factors of the function that we're stressing, not some kind of almighty power to judge that arbitrary constructs are safe or not.
> It's the principle of propagating the safety-determining factors of the function that we're stressing
That's the main function. It's the function that gets called when the program starts. Where do you want to propagate the "safety-determining factors" to?
If I'm just supposed to read the annotations on the `main` function (and those annotations can basically just be a copy of it's body), then why do I need the annotations at all? I could also read the program to determine whether it's safe.
It's because we're dealing with an extreme example in which a program's safety depends on the resolution of an open problem.
If the program's safety depends on the semantics of C and how they've been used in a function, it will be possible to deal with all the conditions upon which a program could be unsafe (in the sense of the standard safety vulnerabilities – like those listed here [0]). Doing so would lead to denouement, so that the annotation to the main function would be empty (meaning none of those bugs can occur).
Programs that might be unsafe should not be verifiable.
> It's because we're dealing with an extreme example in which a program's safety depends on the resolution of an open problem.
It really isn't. The second example is what a reasonable C programmer would produce if you asked them to collect statistics about the chromatic number of random planar graphs. It also isn't based on any open problem. It's overall a very reasonable C program and a small one at that. It's safety also "depends on the semantics of C and how they've been used in a function", specifically on the fact that accessing an array is safe if and only if the index is in bounds. Out of bounds accesses to memory are probably the most common critical vulnerability in C programs, so it is essential that Xr0 prevents them.
I would love to see how you would write this reasonable program in a way that leads to "denouement".
> Programs that might be unsafe should not be verifiable.
Funnily enough, that's exactly what you criticize Rust for. It's not at all clear that writing programs with "denouement" is any less limiting than Rust. In fact, Frama-C (where you also try to write your code in such a way that the annotations become simpler) feels more limiting than Rust.
So will you admit that the first example has been sufficiently addressed? Because I was commenting on the problem involving the Collatz conjecture.
> It's safety also "depends on the semantics of C and how they've been used in a function", specifically on the fact that accessing an array is safe if and only if the index is in bounds. Out of bounds accesses to memory are probably the most common critical vulnerability in C programs, so it is essential that Xr0 prevents them.
True. As you said earlier:
> The safety of this program requires you to prove that `generate_random_planar_graph` always returns a planar graph, that `compute_chromatic_number` correctly identifies the chromatic number and that the chromatic number of every planar graph is less than 5.
This can obviously only be proven if we have the bodies of `generate_random_planar_graph` and `compute_chromatic_number`. Please provide these, and then I can attempt to answer. Because our whole point in Xr0 is that safety comes down to formalising interfaces – without interfaces for these functions we cannot investigate the safety of `main`.
> So will you admit that the first example has been sufficiently addressed? Because I was commenting on the problem involving the Collatz conjecture.
In that this specific program is obviously designed to be extremely hard to prove correct? Yeah. In that most real programs will be easier to prove correct automatically? No.
> This can obviously only be proven if we have the bodies of `generate_random_planar_graph` and `compute_chromatic_number`. Please provide these, and then I can attempt to answer. Because our whole point in Xr0 is that safety comes down to formalising interfaces – without interfaces for these functions we cannot investigate the safety of `main`.
What would be the point of that exactly? We both know that those functions would contain loops and as such Xr0 would be completely unable to verify them. We also know that Xr0 isn't actually able to state that `generate_random_planar_graph` generates a planar graph (other than completely repeating the body in the annotations, I guess). We also both know that Xr0 would not be able to deduce that the chromatic number of planar graphs is less than five.
I already provided two examples of programs the safety of which Xr0 will not be able to verify. I think it's your turn to produce a non-trivial C program that Xr0 will be able to handle.
This discussion really isn't all that enlightening, sadly. Xr0 can't currently handle loops and you haven't produced a single technical argument as to why I should expect Xr0 to be able to handle non-trivial loops in the future.
You also haven't produced a single technical argument as to why Xr0 should succeed where Frama-C failed. The argument that Frama-C is more general while Xr0 is specialized on safety is refuted easily as it is easy to come up with C programs the safety of which depends on arbitrary properties (and I would argue that many if not most real world C programs fall into this category).
One final point – I cannot emphasise strongly enough that we aren't making this for Rust programmers. There's nothing wrong with loving a programming language that has changed the world and what is possible in systems programming. Rust is an advance for systems programming, and it's made incredible strides.
But some programmers (like myself) love working in C, and do not like Rust's restrictions. For such programmers even if the question was one of re-implementation (which we don't think it is) Rust would remain undesirable.
Interesting idea but I have some issues with the code style here. Two problems I see are implicit casts from pointers to integers and use of func() instead of func(void). These are both somewhat minor complaints but they tend to lead to bugs when tested in other environments. In this case I would expect a project aiming to be "C but safe" would at least take the maximum use of existing C safety features. Also the annotations seem a bit cumbersome, I know that's easy to say without providing an alternative but something just doesn't sit right with me about how verbose they are.
Interesting points. Because it's easy to do the type checking at compile time for function prototypes (though we haven't implemented it yet) we haven't felt under pressure to use the `func(void)` notation, which has always felt somewhat uncouth to me.
The verbosity of the annotations is the most jarring thing at the beginning. However, do you find any of them unclear? Because we're optimising for similarity to C before terseness.
I don't find them unclear at all, after reading the introduction I felt pretty comfortable with everything that was going on in the examples. I think this type of approach you're going for can work depending on how it grows to cover more complex cases like loops. I'll be keeping tabs on how your work progresses.
152 comments
[ 0.22 ms ] story [ 245 ms ] threadRust and C++ lately have been particularly quickly moving targets to keep up with, where C is still pretty much the same as C99. The compilers are better, their warnings are better, sanitizer modes are incredible, but the things you type into your text editor to express your program structure are still pretty much the same thing.
Relatively tiny and with a disproportionate number of footguns.
But those are exceptions: I've definitely felt like I've known more than I really did about at least C, C++, Java, Scheme, Python, Go, bash, Javascript, cron, and several assembly variants, and those platforms did little to stop me from learning about my inexperience in difficult, sometimes embarrassing, sometimes expensive ways.
I'm a big fan of more compile time analysis any way it can be done, and whatever can't at runtime. More types, more proofs, more fuzzing, more sanitizers, and also where possible, more restricted execution models than Turing-complete. Any code that can't prove itself correct is a serious liability. I just also like C... it's got many footguns, yes indeed, it's practically constructed out of only footguns, but there are only like 8 of them, and they're all right there waiting for you to get to know them. It's like having a few good sharp knives in your kitchen. You get to know each well, using them one at a time---and if any is missing from the block you pause everything and look around very carefully.
I have 10+ years experience (and consider myself highly proficient) in C#, but my interaction with expression trees is mere hours where I've only once or twice needed to solve a very specific small problem which I could do with a small tweak to code copied from Stack Overflow.
Obviously that's not "the only problem", else there wouldn't be huge style guides forbidding tons of practices to make programs safe for NASA and other such uses, aimed at the expert C programmers hired there.
Also obviously that is not "a problem irrespective of which language we are talking about", unless half-knowing the language has the same impact and the language have the same footguns, which is nowhere near true for other languages versus C. You can "half know" Java and not ever get a buffer overflow. You can know C quite well and still get all kinds of dangerous bugs into the code.
Are any of the many "safe versions of C" getting any traction? There have been so many. It's not a technical problem. It's a mindshare problem.
The future in this area may be something that takes in existing C code and uses a LLM to recognize idioms and annotate. Without some automated way to convert legacy code, this isn't going to happen.
(One big problem with converting to Rust is that Rust's data model is so far from C/C++ that you can't really convert much existing code. You have to rethink the design to fit the affine type model. That's hard.)
https://www.youtube.com/watch?v=Gij9UQy_JEQ
https://github.com/pizlonator/llvm-project-deluge/blob/delug...
Right now I'm ~90% through a major rewrite to use GC instead of isoheaps, because then I'll go from rewrite-a-bit (Fil-C previously required malloc calls to be annotated and for some unions to be changed) to rewrite-nothing (malloc will Just Work and so will unions).
I hope there are others also trying various alternatives. It's too soon for most of these things to tell what traction they may or may not get.
I haven’t looked at what GCC has in a while because I don’t want to get gpl tainted. :-/
https://www.cs.purdue.edu/homes/rompf/papers/xhebraj-ecoop22...
So there's no direct translation from a C++ object hierarchy to Rust structs.
True, but that's likely going to be the case as well to convert to any ”safe version of C” as well, because in the general case the safety of a C program is undecidable: to make it safe, you have to restrict it to a subset of behaviors that can be statically proven as safe, and the borrow checker and “Rust's data model” is just that.
It looks as though the idea is that you can annotate existing code, which is a lot easier than rewriting.
That's not necessarily true though.
Half decent C code already has a coherent memory management strategy. The problem is that humans can't follow even pretty straight-forward memory management strategies 100% of the time. If you have a function that returns memory the caller is required to free, or accepts a parameter that the function takes ownership of, that can be easily expressed but hard to get right every time.
In fact, functions typically document this... in half-decent C code. So we're really talking about formalizing the expression of memory management documentation that already exists and is already understood.
> And you're not getting as much safety bang for your buck for the effort as you would in a rewrite in actually safe language.
I just can't think of what the rational argument for this could be. A complete deep rewrite -- where the new language requires reorganizing the code at a low level so that a lot of existing logic cannot be reused (as-is, or transformed in certain specific ways) -- is extremely costly. It is on the order of the total cost of writing the software in the first place plus the entire cost already spent maintaining it over time. Some costs -- like the goodwill of users/adpoters -- simply cannot be paid again at the same rate. For large scale software there would be numerous regressions over a long period of time, while at the same time the software stops adding many new features, since all the focus will on the rewrite and bugs related to the rewrite. I will stand corrected if there is more than one or two exceptional cases of large scale software making a successful transition of this sort without paying a massive cost.
But rewriting assumes I learn a new language on top of rewriting.
Safe C provides an incremental migration path from unsafe C to safe C. And you don't need to completely rewrite, but instead address the issues flagged, which will often be a lot less work and risk than an actual rewrite in a new language. (This seems obvious to me, but apparently not?)
Would you go into a thread about emacs and say, "Why would anyone use emacs over vi?" And if not, what makes you think you should do that here?
I'm objecting to the disdainful "why would you do it in C?"
Presumably it's easier to rewrite part of your app rather than the whole thing.
But I'm all for a safe version of C17 (or C23/24). It's so disappointing that there isn't a standard memory-safe compiler/runtime/ABI. (And while they're at it, the stack should grow up rather than down.)
Perhaps CHERI or similar will catch on someday. Maybe Apple could try implementing memory checking for clang and Apple Silicon.
Safety annotations is the directions that C++ has been attempting without much success for a while though, so I'm not very optimistic. But I'm always happy to see another attempt.
https://gcc.gnu.org/onlinedocs/gcc/Preprocessor-Options.html
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.)
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.
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 don't see why I would ever choose this over Frama-C which basically does the same (and is actually battle-tested). I just don't see a niche:
- No full control over runtime needed: Java, C#, Python, ...
- Full control over runtime and memory safety: Rust
- Full control over runtime, memory safety and provable absence/presence of certain behaviors (i.e. aerospace, nuclear reactors, ...): Frama-C, CBMC, Astree, ...
Where does Xr0 fit in and how does it differ from existing technology? The fact that they don't even mention any of those tools makes me believe that they are either not aware of them or that they are aware and the difference between this and Frama-C is just syntactic. Not a good look either way.
What is significant about Xr0 is how it applies these old ideas. Xr0 is designed for programmers rather than mathematicians, so to us syntax matters a great, great deal.
I don't think you're under any obligation, I just think that not discussing prior art is a bad look.
> What is significant about Xr0 is how it applies these old ideas.
I don't see anything new about the application of these well-known ideas either. Especially nothing that could explain why Xr0 would be widely used, while Frama-C is extremely niche.
> Xr0 is designed for programmers rather than mathematicians, so to us syntax matters a great, great deal.
Proving (the correctness of code) is an inherently mathematical task. So if by "mathematician" you mean someone who does mathematics, then all of your users will be mathematicians.
See [0] where our reliance on Dijkstra is transparent.
> I don't see anything new about the application of these well-known ideas either. Especially nothing that could explain why Xr0 would be widely used, while Frama-C is extremely niche.
Begin with the fact that Xr0 is written in C and feels like C. We're building it so that C programmers will be able to use it without explicitly learning about formal verification.
> Proving (the correctness of code) is an inherently mathematical task. So if by "mathematician" you mean someone who does mathematics, then all of your users will be mathematicians.
Absolutely true. But what I mean by "mathematician" is a self-conscious mathematician, or at least someone with a background in formal mathematics.
(Edit: forgot to add link.)
[0]: https://xr0.dev/dijkstra-paradox
Mentioning that you're vaguely inspired by Dijkstra is not the same as discussing prior art. And it's not like there isn't enough prior art about "safe C" out there [0, 1, 2, 3, 4, 5, 6, 7, 8, 9].
> Begin with the fact that Xr0 is written in C and feels like C. We're building it so that C programmers will be able to use it without explicitly learning about formal verification.
Most of the people interested in formally verifying their C code will already know about formal verification and absolutely don't care about whether Xr0 is written in C or not.
> But what I mean by "mathematician" is a self-conscious mathematician, or at least someone with a background in formal mathematics.
I'm doubtful Xr0 will be useful for someone without a background in formal verification.
To me, the whole project seems like vapourware. It currently works on an extremely limited subset of C. In fact, this subset is so limited that from a computation theory standpoint, the current capabilities of Xr0 are trivial. Supporting while loops (or general recursion) on the other hand is impossible (from a computation theory standpoint).
Even on this small subset of C it took me five minutes to get an out of memory error and a further five minutes to craft a C program with a double free that passes verification [10].
All this combined with a website that makes great promises about how awesome Xr0 is (or rather going to be) and handwavy explanations about how easy adding the missing features will be that don't hold up to any scrutiny. Dozens of similar projects exist, few of them work at all on non-trivial C programs and all of them require herculean effort (and are thus only used for safety critical software) to correctly annotate C code (often this includes rewriting parts of the code to make the annotations simpler or unnecessary). There is no discussion at all how Xr0 is going to solve the problems that killed these projects.
[0]: https://link.springer.com/chapter/10.1007/978-3-642-03359-9_...
[1]: https://link.springer.com/chapter/10.1007/978-3-540-71316-6_...
[2]: https://link.springer.com/chapter/10.1007/978-3-642-33826-7_...
[3]: https://ieeexplore.ieee.org/document/8543387
[4]: https://dl.acm.org/doi/10.1145/2594291.2594296
[5]: https://link.springer.com/chapter/10.1007/978-3-642-32347-8_...
[6]: https://link.springer.com/chapter/10.1007/978-3-642-20398-5_...
[7]: https://dl.acm.org/doi/10.1145/503272.503286
[8]: https://www.sciencedirect.com/science/article/pii/S157106611...
[9]: https://dl.acm.org/doi/abs/10.1145/3453483.3454036
[10]:
Nice work with the program. However, the only reason it verifies is we haven't yet implemented `||`, so in the parser the phrase `if (x || !y)` is being interpreted as `if (x)` (see [0] for the relevant production). This may seem like another frustrating indiction of how "extremely limited" the subset of C that Xr0 works on is, and indeed it is. But the most important point is there is no logical flaw in Xr0's design here, and no reason whatever that an error of this kind wouldn't be detected. [1] is an equivalent program that shows the logical cogency of our approach (I know it's ugly!).
> I'm doubtful Xr0 will be useful for someone without a background in formal verification.
> Most of the people interested in formally verifying their C code will already know about formal verification and absolutely don't care about whether Xr0 is written in C or not.
We aren't making Xr0 for people (self-consciously) interested in formal verification, but for C programmers interested in safety of the kind that Rust provides. And I can tell you that C programmers prefer their tools in C.
> All this combined with a website that makes great promises about how awesome Xr0 is (or rather going to be) and handwavy explanations about how easy adding the missing features will be that don't hold up to any scrutiny. Dozens of similar projects exist, few of them work at all on non-trivial C programs and all of them require herculean effort (and are thus only used for safety critical software) to correctly annotate C code (often this includes rewriting parts of the code to make the annotations simpler or unnecessary). There is no discussion at all how Xr0 is going to solve the problems that killed these projects.
Fair enough. The proof is in the pudding. Give us a few months. But understand that we have limited resources (this is an open source project and we're working on it part-time). We could either stop and make long-form arguments with full bibliographies or focus on building Xr0 into what we say it's going to be.
[0]: https://git.sr.ht/~lbnz/xr0/tree/master/item/src/ast/gram.y#...
[1]: https://pastebin.com/raw/7EpcUVzv
You should error on constructs you don't yet support. Not doing so makes it very difficult to ascertain how well Xr0 works.
> We could either stop and make long-form arguments with full bibliographies or focus on building Xr0 into what we say it's going to be.
You didn't do either though. You wrote long-form arguments about how awesome Xr0 is (or going to be) and how groundbreaking the idea of "interface formality" is. If instead you actually produced a working prototype (or even any technical argument why such a prototype is feasible) I'd be way less doubtful.
You're right. We should. (We will be adding this as we are able.)
> You didn't do either though. You wrote long-form arguments about how awesome Xr0 is (or going to be) and how groundbreaking the idea of "interface formality" is. If instead you actually produced a working prototype (or even any technical argument why such a prototype is feasible) I'd be way less doubtful.
A 7-point blog post is hardly "long-form" :)
But more to the point, Rust has already achieved this "interface formality", as we state in the second paragraph of this "long-form" piece. That achievement on the part of Rust is indeed groundbreaking. Is it so crazy to claim that this can be replicated for C, without encumbering it with ownership considerations that have no relationship to interface formality?
Fair enough. We have a much more generous definition of "working prototype" than you do. Hopefully one day soon we'll have something that clears yours.
You're not replicating what Rust does, you're replicating what Frama-C does.
Then again, even just replicating what Rust does would be extremely difficult (if not impossible) given the pervasiveness of undefined behavior in C.
> Fair enough. We have a much more generous definition of "working prototype" than you do.
How many useful C programs do you know that require no loops and no binary operators?
Literally on the website. The purpose of the prototype is to show the feasibility of the approach we've taken, not to work on whole programs.
But it doesn't do that. You haven't shown that this approach is able to deal with loops and loops are pretty fundamental to every C program.
Heck, you haven't technically shown that this approach can deal with binary operators. I would love to turn Xr0 into an improptu SAT solver, but without `&&` and `||` that sadly isn't possible right now.
Xr0 is a work in progress, and we'll get there step-by-step.
(I can't find anything about it in this page)
Avoiding UB in single threaded programs is the easy part. It's harder for a low level language like C, but not too hard.
But avoiding UB in multithreaded programs is very very hard. Many "safe" managed languages have UB when you misuse synchronization mechanisms, like Go.
Some languages Java and OCaml manage to avoid UB when you have data races. They do so by disallowing some compiler optimizations. OCaml is the better one in this regard (see the paper "bounding data races in time and space")
Is there any proposal or rough ideas or musings or anything that might suggest how Xr0 could possibly guarantee data race freedom?
Would it be something like Rust's Send & Sync traits? Or something else entirely?
What does surprise is me why someone is so strongly opposed to something that is optional, is a support, and doesn't even get in the way of laying bare the algorithm. It's an annotation to the function declaration, not unlike a return type. Perhaps it's the verbosity?
FWIW I don't think Rust is the answer to this, either. Most software just needs to be written on an even higher abstraction level, with copious redundant safety nets embedded on all levels, performance be damned. It appears that that's the only way we as an industry can reach acceptable quality of software with the average developer that we actually have (as opposed to the hypothetical Zen master).
[0] https://github.com/xr0-org/xr0/releases/tag/v0.15.0
void x(int f) { int * p; p = malloc(1); if(f) { free(p); } if(!f) { free(p); } }
And this doesn't, as expected:
void x(int f) { int * p; p = malloc(1); if(f) { free(p); } if(f) { free(p); } }
edit: another assertion failure:
We've put a fix in for this on a dev branch for now though: https://github.com/xr0-org/xr0/issues/43
I'd be perfectly happy refactoring that so I could have an 'a or b' test (I'm assuming $something means that x(0, 0) not free-ing is correct in real code because nitpicking an illustrative example would be silly).
Though note that I'm sufficiently bad at tracking things right when writing C that I tend to spend most of my debugging time figuring out what stupid mistake I made to cause the current segfault - so I'm probably more willing than average to write code differently if it helps me avoid that ;)
Incidentally, you will notice that Xr0 rejects the program as is, which is correct (because of the double free). It can, however, accept code like the following:
I say "can" because we only have this working on a development branch [0], and there are still some issues we're resolving on this, hopefully by next week.[0]: https://github.com/xr0-org/xr0/tree/fix/nested-branching
void x(int a, int b) { if(! (a != b)) abort();
And the program would be accepted. I'm on my phone and can't verify it though.Great stuff anyway!
Edit: is the algorithm documented anyway? And there is any reason why you guys are not implementing it as a clang/GCC plugin and using the new C and C++ annotation syntax?
We haven't documented the algorithm because it's not the unique part of what we're doing. It works in a very simple-minded way, analysing possible states.
The interesting part is the insight that function interfaces are the boundary along which verification should take place. Applying this idea consistently we escape the combinatorial explosion which tends to plague efforts in this area, because every function can be verified by itself. Notably, Dafny recognised this point before us, and the earliest clear statement we can find regarding it is in Dijkstra's "Notes on Structured Programming", in his chapter "On a Program Model". You may find that illuminating read.
I'm no expert on Clang/GCC and the new annotation syntax for C and C++, but from what I've seen it's not general enough for what we're trying to achieve in Xr0. The safety semantics which are expressed in annotations in Xr0 (see [0] for an example) get very detailed.
[0]: https://xr0.dev/learn#initialisation-of-memory-and-the-clump
Re annotations, I meant the attribute syntax. You can have arbitrary custom syntax in it:
Does it always make sense to strictly enforce code that will be optimized/changed during compilation? Or does Xr0 run after compilation/linking?
How to handle things like unions where you want data in a nice mixed-type struct that is used locally and can also be sent as a stream of uint8_t over a wireless connection? Then, the last function that needs to use the memory frees it. Or is that still fine as long as you malloc once somewhere, free once somewhere, and annotate that the memory region will be accessed as more than one dereferenced type?
Much more important: Will the proposed changes be understandable enough for your average CS undergrad to learn in four months of halfway diligent study? (Then again, you might do away with students taking time to debug improper malloc/free and whatever else falls under the scope of Xr0...)
This doesn't need to be perfect though. Just incrementally better than the status quo.
https://docs.rs/contracts/latest/contracts/
Ada has Design by Contract built into the language (not a library):
https://learn.adacore.com/courses/intro-to-ada/chapters/cont...
DbC is awesome because it formalizes what conditions must exist before and after a piece of code runs and defines who (caller vs. callee) is responsible for what parts.
Though if one wants C and safety and a great language you can get there via, Rust -> Wasm -> C (via wasm2c).
It would be cool to see this applied to say, rsync.
Have you looked at them? Always good to look at prior art, it's not easy what you're trying to do.
Pretty sure I still have the CCured code lying around in a backup somewhere, I downloaded it and played with it long ago. If it's truly not available on the net anywhere, I suppose I can try to dig it up.
The syntax?
If the annotation is basically just a copy of the function body why have any annotation at all?
> So it's not at all clear that we'll run into this.
It might not be clear to you, but if you want to allow any annotation with the same semantics as the body of the function you will run into this.
This is a profound question. Xr0 annotations seem to be copies of the function bodies, but they aren't actually. What they are is a description of the function's safety semantics, the side effects and circumstances under which the function may be relied upon to exhibit well-defined behaviour (under the C Standard).
They only seem to be copies of the bodies because we're dealing with simple examples in the post here and in the tutorial, but we have a much more significant program ready (documenting) that we'll be sharing soon that shows the difference more clearly.
Xr0 is built in explicit reliance upon the powers of programmers to structure code in such a way that the annotations become simpler and simpler as you move up layers of function abstraction. As a simple example, think about what happens when you allocate memory and free it within a function, e.g.
Note that `foo`'s annotation is like a copy of its body, but `bar`'s annotation is very simple, even though it interacts with `foo`, which is only safe if the pointer it returns is handled. So from `baz`'s perspective there are no safety semantics it has to worry about when it interacts with `bar`. The complexity that could lead to safety bugs in `foo` has been completely handled in `bar`.We call this simplifying phenomenon denouement, and well-designed programs exhibit it very strongly. Our belief that programmers can design constructs that tend towards denouement as one moves down the call stack towards `main` is one of the basic reasons we're working on Xr0.
> It might not be clear to you, but if you want to allow any annotation with the same semantics as the body of the function you will run into this.
Yes, but we don't. Only well-defined behaviour according to the C Standard. This is the goal for Xr0 v1.0.0. After that the sky is the limit.
You're constantly dodging the question. If annotations aren't copies of function bodies (which is really the only sensible choice), you need to deduce whether a function body matches the annotations. "Structural similarity" between C and your annotation syntax won't make this easier. In fact, it is impossible to deduce whether two C functions are semantically equivalent even though C is extremely structurally similar to C (you could even argue that C and C are structurally identical).
> Our belief that programmers can design constructs that tend towards denouement as one moves down the call stack towards `main` is one of the basic reasons we're working on Xr0.
So your main criticisms of Rust will mostly also apply to Xr0: You need to rewrite existing C code to make annotations practical (and at that point you might as well reimplement it in Rust) and Xr0 will limit the constructs you will use in your code, because annotations will be impractical for code that isn't written for "denouement".
Maybe I don't understand your point. I am not denying that we're deducing that the body matches the annotations. I'm simply saying that for the restricted case of safety semantics alone, this deduction can be done. Yes, it is impossible to deduce semantic equivalence of arbitrary functions. The question is whether it is possible to deduce that annotations capture the safety semantics of the body. If you have a concrete example it would be helpful here – but for the restricted concerns of safety, not for arbitrary constructs.
> So your main criticisms of Rust will mostly also apply to Xr0: You need to rewrite existing C code to make annotations practical (and at that point you might as well reimplement it in Rust) and Xr0 will limit the constructs you will use in your code, because annotations will be impractical for code that isn't written for "denouement".
Your quote omits the first sentence of the paragraph, which states that "well-designed programs exhibit [denouement] very strongly". Denouement in the sense we're referring to is an absolute theoretical necessity for any safe program, because at some level (of functional abstraction) the safety concerns must be handled, otherwise the program would have a safety vulnerability.
Xr0 definitely limits constructs, but our claim is that the limitation we're imposing is one that reflects the structure of all safe programs. The same cannot be said about Rust's ownership semantics, which limit an enormous number of simple, safe constructs. So the C programs to which one would be adding Xr0 annotations wouldn't need to be rewritten unless a bug has been discovered.
And I'm saying it can't be done, at least not in a fundamentally less tedious and hard way than Frama-C.
> Yes, it is impossible to deduce semantic equivalence of arbitrary functions. The question is whether it is possible to deduce that annotations capture the safety semantics of the body.
It isn't in general.
> If you have a concrete example it would be helpful here – but for the restricted concerns of safety, not for arbitrary constructs.
Safety is not a "restricted concern": You can for every property P easily construct a function that is safe if and only if property P holds. I'll be using Python because this example (which I like) requires arbitrary size integers. You could obviously also implement this in C, you'd just need to implement arbitrary size integers (or use a library that implements them):
This takes as an input an arbitrary positive integer x, searches for a cycle in the Collatz sequence beginning with that number and returns an arbitrary element of that cycle. It is conjectured that for every positive integer this cycle will be 4 -> 2 -> 1 -> 4 -> ... and thus this program is safe if and only if the Collatz conjecture holds.Another example would be a C program that generates random planar graphs, computes their chromatic numbers and then collects statistics about them in an `int statistics[5]`:
The safety of this program requires you to prove that `generate_random_planar_graph` always returns a planar graph, that `compute_chromatic_number` correctly identifies the chromatic number and that the chromatic number of every planar graph is less than 5.However, the main reason why this argument is flawed is it omits the heart of the matter: the annotations. Xr0 empowers programmers to propagate safety semantics. A program that is only safe if the Collatz conjecture holds is (surprise) only safe if the Collatz conjecture holds. So in Xr0 the only requirement we would impose is that this program be augmented with an annotation that communicates that it is only safe if the Collatz conjecture is true.
So the flaw in the reasoning is we haven't claimed that Xr0 can prove arbitrary programs are safe. We've claimed that Xr0 can prove the correspondence between the safety semantics denoted in an annotation and a function body. Above there are no annotations given which would specify "this program is safe only if the Collatz conjecture is true". It shouldn't be hard to prove the correspondence between such an annotation and the program you've written, e.g.:
It's the principle of propagating the safety-determining factors of the function that we're stressing, not some kind of almighty power to judge that arbitrary constructs are safe or not.That's the main function. It's the function that gets called when the program starts. Where do you want to propagate the "safety-determining factors" to?
If I'm just supposed to read the annotations on the `main` function (and those annotations can basically just be a copy of it's body), then why do I need the annotations at all? I could also read the program to determine whether it's safe.
If the program's safety depends on the semantics of C and how they've been used in a function, it will be possible to deal with all the conditions upon which a program could be unsafe (in the sense of the standard safety vulnerabilities – like those listed here [0]). Doing so would lead to denouement, so that the annotation to the main function would be empty (meaning none of those bugs can occur).
Programs that might be unsafe should not be verifiable.
[0]: https://alexgaynor.net/2020/may/27/science-on-memory-unsafet...
It really isn't. The second example is what a reasonable C programmer would produce if you asked them to collect statistics about the chromatic number of random planar graphs. It also isn't based on any open problem. It's overall a very reasonable C program and a small one at that. It's safety also "depends on the semantics of C and how they've been used in a function", specifically on the fact that accessing an array is safe if and only if the index is in bounds. Out of bounds accesses to memory are probably the most common critical vulnerability in C programs, so it is essential that Xr0 prevents them.
I would love to see how you would write this reasonable program in a way that leads to "denouement".
> Programs that might be unsafe should not be verifiable.
Funnily enough, that's exactly what you criticize Rust for. It's not at all clear that writing programs with "denouement" is any less limiting than Rust. In fact, Frama-C (where you also try to write your code in such a way that the annotations become simpler) feels more limiting than Rust.
So will you admit that the first example has been sufficiently addressed? Because I was commenting on the problem involving the Collatz conjecture.
> It's safety also "depends on the semantics of C and how they've been used in a function", specifically on the fact that accessing an array is safe if and only if the index is in bounds. Out of bounds accesses to memory are probably the most common critical vulnerability in C programs, so it is essential that Xr0 prevents them.
True. As you said earlier:
> The safety of this program requires you to prove that `generate_random_planar_graph` always returns a planar graph, that `compute_chromatic_number` correctly identifies the chromatic number and that the chromatic number of every planar graph is less than 5.
This can obviously only be proven if we have the bodies of `generate_random_planar_graph` and `compute_chromatic_number`. Please provide these, and then I can attempt to answer. Because our whole point in Xr0 is that safety comes down to formalising interfaces – without interfaces for these functions we cannot investigate the safety of `main`.
In that this specific program is obviously designed to be extremely hard to prove correct? Yeah. In that most real programs will be easier to prove correct automatically? No.
> This can obviously only be proven if we have the bodies of `generate_random_planar_graph` and `compute_chromatic_number`. Please provide these, and then I can attempt to answer. Because our whole point in Xr0 is that safety comes down to formalising interfaces – without interfaces for these functions we cannot investigate the safety of `main`.
What would be the point of that exactly? We both know that those functions would contain loops and as such Xr0 would be completely unable to verify them. We also know that Xr0 isn't actually able to state that `generate_random_planar_graph` generates a planar graph (other than completely repeating the body in the annotations, I guess). We also both know that Xr0 would not be able to deduce that the chromatic number of planar graphs is less than five.
I already provided two examples of programs the safety of which Xr0 will not be able to verify. I think it's your turn to produce a non-trivial C program that Xr0 will be able to handle.
This discussion really isn't all that enlightening, sadly. Xr0 can't currently handle loops and you haven't produced a single technical argument as to why I should expect Xr0 to be able to handle non-trivial loops in the future.
You also haven't produced a single technical argument as to why Xr0 should succeed where Frama-C failed. The argument that Frama-C is more general while Xr0 is specialized on safety is refuted easily as it is easy to come up with C programs the safety of which depends on arbitrary properties (and I would argue that many if not most real world C programs fall into this category).
But some programmers (like myself) love working in C, and do not like Rust's restrictions. For such programmers even if the question was one of re-implementation (which we don't think it is) Rust would remain undesirable.
The verbosity of the annotations is the most jarring thing at the beginning. However, do you find any of them unclear? Because we're optimising for similarity to C before terseness.