| > 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. |