4 ms·

In my uninformed opinion, the difficulty with code extraction (or going the other way, extracting a theorem prover representation from a program) is shared, mut

by creata 1y ago

In my uninformed opinion, the difficulty with code extraction (or going the other way, extracting a theorem prover representation from a program) is shared, mutable data. All the solutions I've seen (e.g., separation logic) feel clunky as heck. > the fact that you have agree with the abstract model, the fact that the abstract model has to be a good abstract model of your system Regarding seL4 in particular, they've plugged many of those sorts of holes. https://trustworthy.systems/publications/nicta_full_text/7371.pdf https://trustworthy.systems/publications/nicta_full_text/737...

rocqua 1y ago
Rust elliminates shared mutable data. Except for interior mutability and unsafe raw pointers. Even with that asterisk, that makes Rust much more potent in the formal methods space. This has been noted by graydon aswell. I can dig up the reference if someone cares.
- creata 1y ago
  True! Rust proves that you can get very far while only rarely using unrestricted shared mutable data (UnsafeCell). Do you know anything that uses borrowing-like ideas in a theorem proving context?
  - rocqua 1y ago
    I know of Prusti, which is made by Eth Zurich. They use a form of separation logic, their backend (viper) was initially aimed at other languages, mostly go. But now prusti is also aimed at Rust. From what I heard, Rust worked a lot better for them, because a lot of the annotation overhead of Viper was about excluding mutable aliasing. Which rust handily solves. However, last time I checked, I think I saw that Prusti does not currently handle UnsafeCell at all. I don't think that's a fundamental limitation, just a matter prioritized development time.
    - yencabulator 1y ago
      There are so many Rust things that Prusti doesn't understand that applying it to any real world project is still extremely challenging. Kani interacts a little better with real code (see https://model-checking.github.io/kani/rust-feature-support.html https://model-checking.github.io/kani/rust-feature-support.h...), as long as you don't accidentally need e.g. randomness for HashMap DoS protection (https://github.com/model-checking/kani/issues/2423#issuecomment-1925504733 https://github.com/model-checking/kani/issues/2423#issuecomm...). Loops are an utter pain to prove with Kani, though: https://model-checking.github.io/kani/tutorial-loop-unwinding.html https://model-checking.github.io/kani/tutorial-loop-unwindin... -- I believe people are using Verifast for loop-heavy code instead: https://github.com/verifast/verifast https://github.com/verifast/verifast (this hole patchwork of multiple tools mostly consumed as binary downloads is miserable) Here's an attempt to gradually verify the Rust stdlib: https://github.com/model-checking/verify-rust-std https://github.com/model-checking/verify-rust-std
      - rocqua 1y ago
        I love the usage model of Kani. I just dislike the underlying method. Bounded Model Checking cannot take enough advantage of the borrow checker massively curtailing mutable aliasing. But the idea of incremental annotations that require only a little bit of the program to be annotated is great. I think there's a niche for a deductive verification approach that allows for incremental verification.
        yencabulator 1y ago
        Yeah. I'm more a working programmer than an academic, I fundamentally can't care about the fancy theory if the tool isn't usable in real code (I'm looking at you, `verus! { everything is here and utterly miserable to use }`). Put differently: If the "academically superior" tooling isn't good enough, I'll be sticking to testing, fuzzers and sans-I/O style architecture with deterministic simulation testing. The best thing the Rust project could do at this point is to come up with a precondition/postcondition/invariant/etc syntax that a majority of the academics agree with, with the power to express forall and exists and such. Something that is syntactically close to Rust, can be used to annotate normal code, and can be extended tool-by-tool with something that looks like standard attribute macros etc. Then get the academics to focus on the semantics and underlying verification mechanism, while the working programmer gets `debug_assert!` power out of that.
- zozbot234 1y ago
  Yup, and Rust does also have an official Rust Formal Methods Interest Group https://rust-formal-methods.github.io/ https://rust-formal-methods.github.io/ It's likely that there will be significant future developments in this space.

by creata 1y ago

rocqua 1y ago

Rust elliminates shared mutable data. Except for interior mutability and unsafe raw pointers. Even with that asterisk, that makes Rust much more potent in the formal methods space. This has been noted by graydon aswell. I can dig up the reference if someone cares.

creata 1y ago
True! Rust proves that you can get very far while only rarely using unrestricted shared mutable data (UnsafeCell). Do you know anything that uses borrowing-like ideas in a theorem proving context?
- rocqua 1y ago
  I know of Prusti, which is made by Eth Zurich. They use a form of separation logic, their backend (viper) was initially aimed at other languages, mostly go. But now prusti is also aimed at Rust. From what I heard, Rust worked a lot better for them, because a lot of the annotation overhead of Viper was about excluding mutable aliasing. Which rust handily solves. However, last time I checked, I think I saw that Prusti does not currently handle UnsafeCell at all. I don't think that's a fundamental limitation, just a matter prioritized development time.
  - yencabulator 1y ago
    There are so many Rust things that Prusti doesn't understand that applying it to any real world project is still extremely challenging. Kani interacts a little better with real code (see https://model-checking.github.io/kani/rust-feature-support.html https://model-checking.github.io/kani/rust-feature-support.h...), as long as you don't accidentally need e.g. randomness for HashMap DoS protection (https://github.com/model-checking/kani/issues/2423#issuecomment-1925504733 https://github.com/model-checking/kani/issues/2423#issuecomm...). Loops are an utter pain to prove with Kani, though: https://model-checking.github.io/kani/tutorial-loop-unwinding.html https://model-checking.github.io/kani/tutorial-loop-unwindin... -- I believe people are using Verifast for loop-heavy code instead: https://github.com/verifast/verifast https://github.com/verifast/verifast (this hole patchwork of multiple tools mostly consumed as binary downloads is miserable) Here's an attempt to gradually verify the Rust stdlib: https://github.com/model-checking/verify-rust-std https://github.com/model-checking/verify-rust-std
    - rocqua 1y ago
      I love the usage model of Kani. I just dislike the underlying method. Bounded Model Checking cannot take enough advantage of the borrow checker massively curtailing mutable aliasing. But the idea of incremental annotations that require only a little bit of the program to be annotated is great. I think there's a niche for a deductive verification approach that allows for incremental verification.
      - yencabulator 1y ago
        Yeah. I'm more a working programmer than an academic, I fundamentally can't care about the fancy theory if the tool isn't usable in real code (I'm looking at you, `verus! { everything is here and utterly miserable to use }`). Put differently: If the "academically superior" tooling isn't good enough, I'll be sticking to testing, fuzzers and sans-I/O style architecture with deterministic simulation testing. The best thing the Rust project could do at this point is to come up with a precondition/postcondition/invariant/etc syntax that a majority of the academics agree with, with the power to express forall and exists and such. Something that is syntactically close to Rust, can be used to annotate normal code, and can be extended tool-by-tool with something that looks like standard attribute macros etc. Then get the academics to focus on the semantics and underlying verification mechanism, while the working programmer gets `debug_assert!` power out of that.
zozbot234 1y ago
Yup, and Rust does also have an official Rust Formal Methods Interest Group https://rust-formal-methods.github.io/ https://rust-formal-methods.github.io/ It's likely that there will be significant future developments in this space.