[akiarie]

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

[muldvarp]

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

[akiarie]

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.