4 ms·

Yeah, no. They're different things. Formal methods, including static analyzers, can prove the absence of issues in all possible conditions under some assumption

Yeah, no. They're different things. Formal methods, including static analyzers, can prove the absence of issues in all possible conditions under some assumptions. Tests verify that implementation, under the tested conditions, once. You can't replace testing with formal methods, but formal methods are more powerful when they work. That sqlite hasn't found them useful is just a reflection of how absurdly far out they are on the testing spectrum and how complicated the problem domain they're operating in is (very).

gavinhoward 3y ago
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.
derekerdmann 3y ago
Static analyzers are NOT formal methods. Reporting no issues just means your tool didn’t find anything, not that your program is correct.
- adrianN 3y ago
  Formal methods do not necessarily prove the absence of bugs either.
  - worik 3y ago
    > Formal methods do not necessarily prove the absence of bugs either. They can demonstrate the bugs, when found, are in the specifications Or in the methods....
- int0x80 3y ago
  If a static analyzer is sound, which is something that can be mathematically proven (formal method), will find ALL existing issues plus some false positives if it's not complete (which is almost always the case).

gavinhoward 3y ago

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.

derekerdmann 3y ago

Static analyzers are NOT formal methods. Reporting no issues just means your tool didn’t find anything, not that your program is correct.

adrianN 3y ago
Formal methods do not necessarily prove the absence of bugs either.
- worik 3y ago
  > Formal methods do not necessarily prove the absence of bugs either. They can demonstrate the bugs, when found, are in the specifications Or in the methods....
int0x80 3y ago
If a static analyzer is sound, which is something that can be mathematically proven (formal method), will find ALL existing issues plus some false positives if it's not complete (which is almost always the case).