2 ms·
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?
by 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 agoThere'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.