[akiarie]

> The point of interfaces is usually to hide underlying complexity. What's the point of interfaces that are just as complicated as their implementation?

This is a pivotal question and our answer to it exposes one of our basic assumptions. Interfaces do hide underlying complexity, but that is not all that they do. They define our interaction with abstractions, which not only hide complexity, but reduce it by "abstracting". So what we find in practice is that the interfaces are not as complicated as the code, because all they define is what the higher levels of abstraction need to know to interact abstractly with the lower levels.

> One of the things I personally like about Rust is that its rules are very simple and still capture 95% of all situations I find myself in. Adding the complexity of having to write your own formal specifications for the remaining 5% doesn't seem like it's worth the effort.

Well this is great. If you like Rust, there's nothing wrong with that. But many C programmers don't feel this way.

> Xr0 will also either 1) reject programs that are safe or 2) accept programs that are unsafe. An (computable) algorithm that decides for every C program whether it is safe or not is mathematically impossible. Start implementing loops and you'll quickly see why the idea of provable correctness without any restrictions is doomed to fail.

Insightful again! This is all true. Note, however, that we aren't claiming not to impose restrictions. We're claiming that the restrictions should concentrate at a different place than where they concentrate in Rust. They should orbit around the interfaces. Xr0 is certainly imposing restrictions there.

Moreover, we are in no way suggesting/claiming that we can deduce the safety of arbitrary C programs, which is the whole reason the annotations are required. We're claiming that we can help programmers who already understand why their code is safe express these reasons in relatively-simple annotations, and use these to verify their reasoning.

Edit: typo.

[muldvarp]

> We're claiming that the restrictions should concentrate at a different place than where they concentrate in Rust. They should orbit around the interfaces.

Rust's restrictions can also be interpreted as restrictions on interfaces. A function taking (a non-`Copy` type) by value is a function that Xr0 would annotate as `free`ing that variable, for example.

> Moreover, we are in no way suggesting/claiming that we can deduce the safety of arbitrary C programs, which is the whole reason the annotations are required.

You are claiming that Xr0 will deduce that a function matches its annotations. If those annotations are "this function has property P", you'll have to deduce whether the function actually has property P. This can be augmented by inline annotations (i.e. annotations for code, not interfaces) and those will likely become necessary once you implement loops. But at that point you'll have reinvented Frama-C and you'll realize why Frama-C isn't used outside of safety-critical software: It's both hard and exhausting to use.

[akiarie]

> Rust's restrictions can also be interpreted as restrictions on interfaces. A function taking (a non-`Copy` type) by value is a function that Xr0 would annotate as `free`ing that variable, for example.

Yes they can, and we said this in the article, "The remarkable safety guarantees that Rust provides are consequent to something much deeper than its ownership rules: Rust empowers programmers to formalise and verify the semantics of pointer usage at the interface boundary between functions. If interface formality is the fundamental determinant of safety, systems language design should focus directly on it rather than on any other criterion, including ownership."

The point we're stressing, though, is that the restrictions in Rust do not focus on the interfaces, but on the ownership principle. So we're advocating for language design to ignore ownership considerations and deal with the interfaces as the important point.

> You are claiming that Xr0 will deduce that a function matches its annotations. If those annotations are "this function has property P", you'll have to deduce whether the function actually has property P. This can be augmented by inline annotations (i.e. annotations for code, not interfaces) and those will likely become necessary once you implement loops. But at that point you'll have reinvented Frama-C and you'll realize why Frama-C isn't used outside of safety-critical software: It's both hard and exhausting to use.

Again, I agree with most of this (except the cynicism). We have done some serious experiments with implementing loops and immediately saw that we would need to annotate the loops also (with at least some kind of invariants).

The comparison to Rust is actually a whole lot more helpful than that to Frama-C. Why is Rust able to deliver safety guarantees without becoming "hard and exhausting"? Our argument is that it is the interface formality issue that really determines safety. If this is so, why should it be "hard and exhausting" to be empowered with the ability to be formal at the interfaces concerning the things that influence safety?

The fact that we're using annotations does not mean that Xr0 is equivalent to Frama-C. To point to one important difference, we're focused on securing safety, whereas Frama-C is a general purpose tool for arbitrary correctness considerations. If Xr0 does grow to deal with such arbitrary correctness concerns, it is possible that it will become "hard and exhausting" like Frama-C, because of the inherent difficulty of complete verification. But while we're focused on safety alone, there's no reason why we can't offer something that is at most of the same difficulty level of working in Rust. Xr0's annotations are not "this function has property P" where P is arbitrary. They are "this function has well-defined behaviour according to the C standard under these circumstances". That is a much more limited kind of condition to validate.

[muldvarp]

> Our argument is that it is the interface formality issue that really determines safety.

Frama-C also does "interface formality". Chapter 3 (i.e. the first chapter after the one telling you how to install Frama-C) of the Frama-C WP tutorial is literally called "function contracts" and explains how to use ACSL to annotate pre- and post-conditions on functions.

> The comparison to Rust is actually a whole lot more helpful than that to Frama-C.

Your approach is way more similar to Frama-C than to Rust. The difference between Rust and Frama-C is that Frama-C allows you to specify arbitrary constraints, while Rust only allows you to specify very few and specific constraints. That may feel limiting (as you have pointed out) but that's also what makes it possible to deduce whether the function actually satisfies these constraints without having to annotate every loop (which is tedious for simple loops and hard for complex ones).

> If this is so, why should it be "hard and exhausting" to be empowered with the ability to be formal at the interfaces concerning the things that influence safety?

Annotating functions can be hard if the pre- or post-conditions of that function are hard to formalize (e.g. "this function returns the first element of a loop in the given linked list or null if no loop exists"), but having to annotate interfaces isn't what makes Frama-C hard to use. Frama-C is hard to use because it is hard to get it to accept that the function actually satisfies the function contract and this is a problem you will also face.

> To point to one important difference, we're focused on securing safety, whereas Frama-C is a general purpose tool for arbitrary correctness considerations. [...] They are "this function has well-defined behaviour according to the C standard under these circumstances". That is a much more limited kind of condition to validate.

Undefined behavior is extremely pervasive in C. If one of Xr0's goals is to verify that a C program does not exhibit undefined behavior (and it has to, given that undefined behavior is anything but safe) then you'll have to verify properties such as "this addition doesn't overflow", "this value is never INT_MIN", "this value is never negative", "this value is never zero", "a is less than b", ...

There will barely be any difference between verifying that a function has "well-defined behavior under these circumstances" and full verification.