3 ms·

Can you give a run down on formal verification?

seanwilson 7y ago
So say you were writing a sorting algorithm and with unit tests (perhaps with TDD) you wrote tests like: - sort([]) should produce [] - sort([1]) should produce [1] - sort([1,3,2]) should produce [1,2,3] - sort([1,5,6,2,3,4]) should produce [1,2,3,4,5,6] You would test a few values and edge cases until you were confident it works for all lists. However, you can't be 100% sure that there's some list out there like [5,5,5,5,1] that doesn't get sorted properly. With formal verification, you can actually test it sorts for all possible lists with a mathematical proof. You write a maths proof that shows a property like the following holds: - For all lists X, the result of sort(X) will be a permutation of X that is sorted. For example, the proof could take the form of proof by induction where every step in the proof is confirmed correct by the machine (see Coq, Isabelle for more info). When you were doing maths at school, you probably had exercises where you tried a few examples to see if an equation you came up with might hold in general and then you would write a proof to showed it worked for all possible cases (e.g. with induction, by case analysis). The former is similar to unit testing and the latter is similar to formal verification. My point was there's a spectrum of how rigorous your tests are. People talk about TDD like it's the holy grail sometimes but it's nowhere close to how rigorous you can be. If you've tried some formal verification though, you'll realise it's far too expensive for most projects. Likewise, TDD doesn't make sense for all projects. You have to pick your tradeoffs e.g. between time to market vs cost vs ease of refactoring later vs how rigorous the testing is.
- Izkata 7y ago
  > You would test a few values and edge cases until you were confident it works for all lists. However, you can't be 100% sure that there's some list out there like [5,5,5,5,1] that doesn't get sorted properly. For the curious, something like this has happened before - and was found with formal verification: http://www.envisage-project.eu/proving-android-java-and-python-sorting-algorithm-is-broken-and-how-to-fix-it/ http://www.envisage-project.eu/proving-android-java-and-pyth...
- stingraycharles 7y ago
  Isn’t this formal verification more for algorithms than implementations? Eg if I have to use Coq to prove my code works, what use is that for my C application? Porting the code to Coq seems to defeat the point of formal verification, I can much better use some property based testing method.
  - seanwilson 7y ago
    There's lots of options. You can write an implementation in Coq (it has its own functional language you code in), prove it correct in Coq and then "extract" (like transpiling) it to another language like OCaml for executing. There's ways to map C code into Coq to prove it's correct as well. All of this is machine checked. See the sel4 kernel to get more of a feel for it. Property based testing sits somewhere between regular software testing with unit tests and theorem proving on the spectrum. It's much less time intensive to do but much less rigorous. My point isn't that formal verification is better than everything. It has its trade-offs, just like TDD.

So say you were writing a sorting algorithm and with unit tests (perhaps with TDD) you wrote tests like: - sort([]) should produce [] - sort([1]) should produce [1] - sort([1,3,2]) should produce [1,2,3] - sort([1,5,6,2,3,4]) should produce [1,2,3,4,5,6] You would test a few values and edge cases until you were confident it works for all lists. However, you can't be 100% sure that there's some list out there like [5,5,5,5,1] that doesn't get sorted properly. With formal verification, you can actually test it sorts for all possible lists with a mathematical proof. You write a maths proof that shows a property like the following holds: - For all lists X, the result of sort(X) will be a permutation of X that is sorted. For example, the proof could take the form of proof by induction where every step in the proof is confirmed correct by the machine (see Coq, Isabelle for more info). When you were doing maths at school, you probably had exercises where you tried a few examples to see if an equation you came up with might hold in general and then you would write a proof to showed it worked for all possible cases (e.g. with induction, by case analysis). The former is similar to unit testing and the latter is similar to formal verification. My point was there's a spectrum of how rigorous your tests are. People talk about TDD like it's the holy grail sometimes but it's nowhere close to how rigorous you can be. If you've tried some formal verification though, you'll realise it's far too expensive for most projects. Likewise, TDD doesn't make sense for all projects. You have to pick your tradeoffs e.g. between time to market vs cost vs ease of refactoring later vs how rigorous the testing is.

Izkata 7y ago
> You would test a few values and edge cases until you were confident it works for all lists. However, you can't be 100% sure that there's some list out there like [5,5,5,5,1] that doesn't get sorted properly. For the curious, something like this has happened before - and was found with formal verification: http://www.envisage-project.eu/proving-android-java-and-python-sorting-algorithm-is-broken-and-how-to-fix-it/ http://www.envisage-project.eu/proving-android-java-and-pyth...
stingraycharles 7y ago
Isn’t this formal verification more for algorithms than implementations? Eg if I have to use Coq to prove my code works, what use is that for my C application? Porting the code to Coq seems to defeat the point of formal verification, I can much better use some property based testing method.
- seanwilson 7y ago
  There's lots of options. You can write an implementation in Coq (it has its own functional language you code in), prove it correct in Coq and then "extract" (like transpiling) it to another language like OCaml for executing. There's ways to map C code into Coq to prove it's correct as well. All of this is machine checked. See the sel4 kernel to get more of a feel for it. Property based testing sits somewhere between regular software testing with unit tests and theorem proving on the spectrum. It's much less time intensive to do but much less rigorous. My point isn't that formal verification is better than everything. It has its trade-offs, just like TDD.