3 ms·

Don't get me wrong; I'm a fan of formal methods, when they can work. But you're also weakening your own point; you admit that if you test enough, they don't wo

Don't get me wrong; I'm a fan of formal methods, when they can work. But you're also weakening your own point; you admit that if you test enough, they don't work as well, and you also admit that they work less well the more complicated things get. The other problem is showing that the artifact you proved is the same artifact that you are using. The enormous amount of effort put in by the seL4 people is proof that that is non-trivial, and seL4 is tiny compared to SQLite. So when you say, "formal methods are more powerful when they work," you are right, but "when they work" is carrying a lot of weight.

nicoburns 3y ago
Stronger type systems can get you a lot of the benefits of formal methods with very little work. A SQLite level test suite is probably still better, but very few projects have the time or budget to do that.
- gavinhoward 3y ago
  I agree. And that's one thing I disagree with the SQLite guys on; I build with all warnings enabled to get me a "stronger" type system in C. I get stronger warnings against pointer casting and things like that. But "a lot of the benefits" is still maybe about half of the benefits of full formal methods.
nanolith 3y ago
seL4 primarily uses a proof assistant, which is a MUCH harder way to go about formal methods. It's thorough, sure, but for 80% to 95% of the average code base, model checking would work just fine. It's not a good metric to claim that since seL4 did things the hard way that any formal methods project is impractical. That's simply not the case. seL4 is an OS with very specific process isolation requirements that they wanted to model using a proof assistant. SQLite wouldn't need that level of instrumentation in proofs. Most of SQLite could be formally verified using a model checker. Model checkers, such as CBMC and others, can provide safety checks without needing to build constructive proofs. In practice, constructive proofs are only needed for things that model checking can't solve, such as data structures and algorithms requiring recursion or looping. In these cases, a proof assistant with inductive theorems can be used to extract equivalent software that can be proven to be safe in the recursive case. But, if your goal is just to check to see if your code is safe, which goes beyond the limits for most developers to test with unit testing alone, then model checking is good enough. I use model checking in all of the C software I write, and have done so for nearly a decade now. It's not a question of "when they work". I demand that it works, just as I demand that unit testing works, so I make it work. It adds, perhaps, 30% development overhead. Model checking makes my code safer because it gives me the ability to track function contracts, UB in integer and pointer math, and resource ownership. Attempting to do this with unit testing requires that I'm smart enough, every time, to create the right tests for things that simply don't show up when I look at code coverage reports. That classical trivial test of inputs using 0, -1, numbers close to or equal to integer limits, etc., don't necessarily catch the limit hole caused by wonky pointer math. The coverage report shows 100%, and code reviewers may miss it. But, the model checker doesn't. I used to think I was a great programmer. Then, I spent a couple years running my code through a model checker. Now, I know better.
- gavinhoward 3y ago
  > It's not a question of "when they work". I demand that it works, just as I demand that unit testing works, so I make it work. Sure, if you can. And I use such checkers too. But for a lot of people, the false positive false negative rates are still high. That's why tests can be better: there's no false positive or false negative. > The coverage report shows 100%, and code reviewers may miss it. But, the model checker doesn't. This is unfortunately completely naive. Of course model checkers miss things.
  - nanolith 3y ago
    > This is unfortunately completely naive. Of course model checkers miss things. Perhaps you're thinking of a static analyzer which is something different. The ENTIRE POINT of a model checker is that it translates the program into a constraint solver. Can it miss things? Yes, if there is a bug in the translation. It can't be trusted for things that it can't detect, but a model check is equivalent to a constructive proof. It just doesn't have some tools like induction that make constructive proofs necessary in cases where model checking fails. There is no such thing as a magic tool. The scenarios under model check must be properly built, just like any formal proof. But, a constructive proof assistant and a SMT solver are both forms of proof engines. A model checker uses an SMT solver. The seL4 team uses model checking as well, in the generated code. They trust model checking in these cases because it's thorough. If it missed things, it would be pointless to use.
    - gavinhoward 3y ago
      > Can it miss things? Yes, if there is a bug in the translation. So you're saying humans are bad at writing software, but good at writing translations for model checkers? I disagree. The reason model checkers miss things is because of humans. > The seL4 team uses model checking as well, in the generated code. I am aware, trust me. Are you aware how much effort they had to expend to do that?
      - nanolith 3y ago

nicoburns 3y ago

Stronger type systems can get you a lot of the benefits of formal methods with very little work. A SQLite level test suite is probably still better, but very few projects have the time or budget to do that.

gavinhoward 3y ago
I agree. And that's one thing I disagree with the SQLite guys on; I build with all warnings enabled to get me a "stronger" type system in C. I get stronger warnings against pointer casting and things like that. But "a lot of the benefits" is still maybe about half of the benefits of full formal methods.

nanolith 3y ago

seL4 primarily uses a proof assistant, which is a MUCH harder way to go about formal methods. It's thorough, sure, but for 80% to 95% of the average code base, model checking would work just fine. It's not a good metric to claim that since seL4 did things the hard way that any formal methods project is impractical. That's simply not the case. seL4 is an OS with very specific process isolation requirements that they wanted to model using a proof assistant. SQLite wouldn't need that level of instrumentation in proofs. Most of SQLite could be formally verified using a model checker. Model checkers, such as CBMC and others, can provide safety checks without needing to build constructive proofs. In practice, constructive proofs are only needed for things that model checking can't solve, such as data structures and algorithms requiring recursion or looping. In these cases, a proof assistant with inductive theorems can be used to extract equivalent software that can be proven to be safe in the recursive case. But, if your goal is just to check to see if your code is safe, which goes beyond the limits for most developers to test with unit testing alone, then model checking is good enough. I use model checking in all of the C software I write, and have done so for nearly a decade now. It's not a question of "when they work". I demand that it works, just as I demand that unit testing works, so I make it work. It adds, perhaps, 30% development overhead. Model checking makes my code safer because it gives me the ability to track function contracts, UB in integer and pointer math, and resource ownership. Attempting to do this with unit testing requires that I'm smart enough, every time, to create the right tests for things that simply don't show up when I look at code coverage reports. That classical trivial test of inputs using 0, -1, numbers close to or equal to integer limits, etc., don't necessarily catch the limit hole caused by wonky pointer math. The coverage report shows 100%, and code reviewers may miss it. But, the model checker doesn't. I used to think I was a great programmer. Then, I spent a couple years running my code through a model checker. Now, I know better.

gavinhoward 3y ago
> It's not a question of "when they work". I demand that it works, just as I demand that unit testing works, so I make it work. Sure, if you can. And I use such checkers too. But for a lot of people, the false positive false negative rates are still high. That's why tests can be better: there's no false positive or false negative. > The coverage report shows 100%, and code reviewers may miss it. But, the model checker doesn't. This is unfortunately completely naive. Of course model checkers miss things.
- nanolith 3y ago
  > This is unfortunately completely naive. Of course model checkers miss things. Perhaps you're thinking of a static analyzer which is something different. The ENTIRE POINT of a model checker is that it translates the program into a constraint solver. Can it miss things? Yes, if there is a bug in the translation. It can't be trusted for things that it can't detect, but a model check is equivalent to a constructive proof. It just doesn't have some tools like induction that make constructive proofs necessary in cases where model checking fails. There is no such thing as a magic tool. The scenarios under model check must be properly built, just like any formal proof. But, a constructive proof assistant and a SMT solver are both forms of proof engines. A model checker uses an SMT solver. The seL4 team uses model checking as well, in the generated code. They trust model checking in these cases because it's thorough. If it missed things, it would be pointless to use.
  - gavinhoward 3y ago
    > Can it miss things? Yes, if there is a bug in the translation. So you're saying humans are bad at writing software, but good at writing translations for model checkers? I disagree. The reason model checkers miss things is because of humans. > The seL4 team uses model checking as well, in the generated code. I am aware, trust me. Are you aware how much effort they had to expend to do that?
    - nanolith 3y ago