3 ms·

> Formal verification simply doesn’t scale to global properties This is an assertion you are making with absolutely no evidence, and also totally self-contradi

> Formal verification simply doesn’t scale to global properties This is an assertion you are making with absolutely no evidence, and also totally self-contradictory with your statement "Rust’s borrow checker is nothing else but an included proof assistant for rust code". While we're at it, also Ada does this, which has long been used for large scale mission critical applications where formal assurances are necessary (with even more available optional safeties than rust provides).

zozbot234 5y ago
Formal verification doesn't scale to global properties in the general case. Global properties that are simple and type-like (in that they match the syntactic structure of the program in a fully "compositional" way, like Rust lifetimes) can be checked with comparable ease. Complex properties can often be checked within a single, self-contained, small-enough program module. Trying to do both at the same time - check complex properties globally - is highly problematic. That's why the Rust borrow checker has to make simplifying assumptions, and use 'unsafe' as an escape hatch.
- staticassertion 5y ago
  I'm not really convinced that this is true. I think you're brushing up against Rice's theorem, which is that proving arbitrary properties about arbitrary programs is equivalent to the halting problem. That's why we constrain languages with type systems, which limits any typed language from expressing arbitrary turing complete programs. Proof assistance is sort of irrelevant. Types and proofs are related, as denoted by the curry howard correspondance. The real issue with "throwawaymaths"' point is that they're saying "use proof assistants" to people who are using proof assistants. SEL4 is a terrible example of a success story, as it took ages to complete, and then there was immediately a bug found in a class they weren't looking for - because rice's theorem. They're clearly advocating for the use of specific and explicit proof assistants, which is fine and a totally reasonable thing to advocate for, but in no way is related to rust or the discussion, which is why I chose not to engage.
kaba0 5y ago
I meant to write every global property due to Rice’s theorem. And I don’t believe my claim is unsupported, the largest formally verified program is the mentioned sel4, which is still tiny compared to even the smallest of business apps and was written by domain experts over multiple years. Restricting a problem to a subset is like the numero uno step to solve any hard problem - and this is what rust basically mandate. It won’t provide bug-free programs, but it can reliably prove the absence of memory bugs and data races due to the borrow checker, which can do its work on function-scope, since all the relevant information is encoded in the function’s generic lifetime arguments.
woodruffw 5y ago
These claims aren’t contradictory when you understand the domain in question: formal verification of C abstract semantics doesn’t scale particularly well. Rust (and Ada) both have restricted memory semantics (particularly around aliasing) that effectively eliminate some of the hardest problems in whole-program static analysis.

zozbot234 5y ago

Formal verification doesn't scale to global properties in the general case. Global properties that are simple and type-like (in that they match the syntactic structure of the program in a fully "compositional" way, like Rust lifetimes) can be checked with comparable ease. Complex properties can often be checked within a single, self-contained, small-enough program module. Trying to do both at the same time - check complex properties globally - is highly problematic. That's why the Rust borrow checker has to make simplifying assumptions, and use 'unsafe' as an escape hatch.

staticassertion 5y ago
I'm not really convinced that this is true. I think you're brushing up against Rice's theorem, which is that proving arbitrary properties about arbitrary programs is equivalent to the halting problem. That's why we constrain languages with type systems, which limits any typed language from expressing arbitrary turing complete programs. Proof assistance is sort of irrelevant. Types and proofs are related, as denoted by the curry howard correspondance. The real issue with "throwawaymaths"' point is that they're saying "use proof assistants" to people who are using proof assistants. SEL4 is a terrible example of a success story, as it took ages to complete, and then there was immediately a bug found in a class they weren't looking for - because rice's theorem. They're clearly advocating for the use of specific and explicit proof assistants, which is fine and a totally reasonable thing to advocate for, but in no way is related to rust or the discussion, which is why I chose not to engage.

kaba0 5y ago

I meant to write every global property due to Rice’s theorem. And I don’t believe my claim is unsupported, the largest formally verified program is the mentioned sel4, which is still tiny compared to even the smallest of business apps and was written by domain experts over multiple years. Restricting a problem to a subset is like the numero uno step to solve any hard problem - and this is what rust basically mandate. It won’t provide bug-free programs, but it can reliably prove the absence of memory bugs and data races due to the borrow checker, which can do its work on function-scope, since all the relevant information is encoded in the function’s generic lifetime arguments.

woodruffw 5y ago

These claims aren’t contradictory when you understand the domain in question: formal verification of C abstract semantics doesn’t scale particularly well. Rust (and Ada) both have restricted memory semantics (particularly around aliasing) that effectively eliminate some of the hardest problems in whole-program static analysis.