3 ms·

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 o

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.

muldvarp 2y ago
> 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.
- akiarie 2y ago
  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. [0]: https://alexgaynor.net/2020/may/27/science-on-memory-unsafety-and-security/ https://alexgaynor.net/2020/may/27/science-on-memory-unsafet...
  - muldvarp 2y ago
    > 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.
    - akiarie 2y ago
      > It really isn't. The second example is ... 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`.
      - 2y ago

muldvarp 2y ago

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

akiarie 2y ago
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. [0]: https://alexgaynor.net/2020/may/27/science-on-memory-unsafety-and-security/ https://alexgaynor.net/2020/may/27/science-on-memory-unsafet...
- muldvarp 2y ago
  > 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.
  - akiarie 2y ago
    > It really isn't. The second example is ... 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`.
    - 2y ago