5 ms·

Sibling comments laments (obliquely) formal methods aren't more ubiquitous. The reason is not cost. It can also be cost but usually things that cost a lot peopl

Sibling comments laments (obliquely) formal methods aren't more ubiquitous. The reason is not cost. It can also be cost but usually things that cost a lot people sometimes still want (lambos, ferraris) but almost no one even wants formal methods. Here's the reason: > For example, the formal proofs of the seL4 kernel establish amongst other things that the implementation C code precisely matches an abstract model of the kernel. This is a really powerful and impressive result, but to understand it, you have to study the formal model in detail. No not the complexity of understanding the abstract model - 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. This is what everyone says about TLA+, that sure you can prove a raft spec has no deadlock but you can't extract an implementation from the same spec. Yes I know some proof systems do actually let you extract (fsharp) but they are few and far between because proof languages are to programming languages as the NBA is to college ball: a whole different league of precision/specification (so lots of things cannot be translated). I don't have answer/solution. Not saying that I do. The article is good though, reads like any basic sales journey (which isn't a bad thing).

zmgsabst 1y ago
I’m not convinced they’re that different — there’s a spectrum from type systems to Agda/Coq. Most developers use some kind of formal method (types); and probably correctly conclude that more formality doesn’t aid their case. That’s okay — but I think we do everyone a disservice by posing these as binaries or different leagues, when it’s a spectrum with lots of different and partial applications (eg, there’s utility in proving properties of your math even without a full formal proof). That false binary is what slows adoption more than anything — at least in my experience.
- almostgotcaught 1y ago
  > I’m not convinced they’re that different — there’s a spectrum from type systems to Agda/Coq. I didn't say you couldn't write code in proof languages, I just said (implied) it would be extremely tedious/onerous.
  - deleted 1y ago
    [deleted]
- rocqua 1y ago
  There's a benefit to types beyond correctness. It helps make code understandable locally. And that helps speed up code development, by making changes to code much faster. I think this might be the real value of formal methods. Not correctness, but speed of itteration. That does affect what kind of formal methods do and don't help. Which really matches what the article said on delivering value with just a small amount of effort.
  - LegionMammal978 1y ago
    Often, a program can accumulate so many types that little logic is present in the code proper, but now you need an encyclopedic knowledge of the types and all their dependencies to work with them, since the complexity has just been shifted and not removed. I'm mainly thinking of the gnarly template errors you'll see in C++, or trait errors in Rust, caused by heavy use of type-based logic. Poor error formatting can exacerbate this, but ultimately you still need an understanding of all the type constraints to do anything, and documentation is often unhelpful since it's diced up into a dozen little pieces. That is to say, the local optimum of "making changes to code much faster" can be reached pretty early in the process of increasing specification, and many existing projects (IMHO) have overshot that mark to little benefit. So I'm inclined to be skeptical about FM's value proposition, unless it can be applied in an very progressive manner in places where extra specification makes the most sense.
    - zmgsabst 1y ago
      Your last point is what I was trying to get at — eg, reasoning just about your math expressions. https://herbie.uwplse.org/ https://herbie.uwplse.org/ I think that FM (beyond basic typing) is best used sparingly to address particularly sensitive cases — eg, floating point stability in modeling. But our discussion usually doesn’t include incremental or partial usage, unfortunately.
      - rocqua 1y ago
        I've been looking at incremental / partial formal verification based on 'assert'-like statements. Kani for rust has an interface close to what I imagine. But I'd like to use deductive verification (something like hoare / seperation logic) instead. This means the developer gets to decide what is important enough to try to assert. It's likely the developer will need to add sub-lemma's to get the assert to be proven, and I suspect some of these will need to be in the form of 'assumptions / requirements' at the start of a function, which then need to be confirmed at all call-sites. A big downside here is that some things you'd like to prove often don't fit into boolean expressions in the underlying language. For example, universal / existential quantifiers aren't available (but are implicit in the formal prover, so can be hacked into). You also don't have predicates for 'this address has been allocated / initialized' nor any other predicates that let you say a value is constant. Similarly, there are no temporal quantifiers available. I'm hoping that the above is not too limiting in practice. The fact that developers already user 'assert' statements does suggest that normal boolean expressions are already valuable.
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

zmgsabst 1y ago

I’m not convinced they’re that different — there’s a spectrum from type systems to Agda/Coq. Most developers use some kind of formal method (types); and probably correctly conclude that more formality doesn’t aid their case. That’s okay — but I think we do everyone a disservice by posing these as binaries or different leagues, when it’s a spectrum with lots of different and partial applications (eg, there’s utility in proving properties of your math even without a full formal proof). That false binary is what slows adoption more than anything — at least in my experience.

almostgotcaught 1y ago
> I’m not convinced they’re that different — there’s a spectrum from type systems to Agda/Coq. I didn't say you couldn't write code in proof languages, I just said (implied) it would be extremely tedious/onerous.
- deleted 1y ago
  [deleted]
rocqua 1y ago
There's a benefit to types beyond correctness. It helps make code understandable locally. And that helps speed up code development, by making changes to code much faster. I think this might be the real value of formal methods. Not correctness, but speed of itteration. That does affect what kind of formal methods do and don't help. Which really matches what the article said on delivering value with just a small amount of effort.
- LegionMammal978 1y ago
  Often, a program can accumulate so many types that little logic is present in the code proper, but now you need an encyclopedic knowledge of the types and all their dependencies to work with them, since the complexity has just been shifted and not removed. I'm mainly thinking of the gnarly template errors you'll see in C++, or trait errors in Rust, caused by heavy use of type-based logic. Poor error formatting can exacerbate this, but ultimately you still need an understanding of all the type constraints to do anything, and documentation is often unhelpful since it's diced up into a dozen little pieces. That is to say, the local optimum of "making changes to code much faster" can be reached pretty early in the process of increasing specification, and many existing projects (IMHO) have overshot that mark to little benefit. So I'm inclined to be skeptical about FM's value proposition, unless it can be applied in an very progressive manner in places where extra specification makes the most sense.
  - zmgsabst 1y ago
    Your last point is what I was trying to get at — eg, reasoning just about your math expressions. https://herbie.uwplse.org/ https://herbie.uwplse.org/ I think that FM (beyond basic typing) is best used sparingly to address particularly sensitive cases — eg, floating point stability in modeling. But our discussion usually doesn’t include incremental or partial usage, unfortunately.
    - rocqua 1y ago
      I've been looking at incremental / partial formal verification based on 'assert'-like statements. Kani for rust has an interface close to what I imagine. But I'd like to use deductive verification (something like hoare / seperation logic) instead. This means the developer gets to decide what is important enough to try to assert. It's likely the developer will need to add sub-lemma's to get the assert to be proven, and I suspect some of these will need to be in the form of 'assumptions / requirements' at the start of a function, which then need to be confirmed at all call-sites. A big downside here is that some things you'd like to prove often don't fit into boolean expressions in the underlying language. For example, universal / existential quantifiers aren't available (but are implicit in the formal prover, so can be hacked into). You also don't have predicates for 'this address has been allocated / initialized' nor any other predicates that let you say a value is constant. Similarly, there are no temporal quantifiers available. I'm hoping that the above is not too limiting in practice. The fact that developers already user 'assert' statements does suggest that normal boolean expressions are already valuable.

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