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)"?
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.