3 ms·

It's certainly still being used. I use bounded model checking, which performs a kind of symbolic execution using an SMT solver. For more complex things that ar

It's certainly still being used. I use bounded model checking, which performs a kind of symbolic execution using an SMT solver. For more complex things that aren't as easy to model check, such as the formal verification of a deeply recursive algorithm or a cryptographic algorithm against specification, I'll use Coq or Lean to define an abstract machine model, then either extract code from this model into C, C++, or machine code, or when something hand written is required, extract code into an intermediate format, then import hand written source code into this same format, then prove the two equivalent. Fuzzing is useful, but fuzzing serves different goals. With fuzzing, you can find execution paths that are incorrect, with a reproducer. However, these paths must be reachable with the fuzzer within the search depth defined. Fuzzing can find failure cases, but it can't prove the absence of such cases. Model checking can be significantly faster if well engineered, and it can be used to prove the absence of classes of errors. The same goes with constructive proofs in a proof assistant. The two approaches are complementary. One doesn't replace the other.

skulk 2y ago
> I'll use Coq or Lean to define an abstract machine model, then either extract code from this model into C, C++, or machine code, Do you have any worked examples or blog posts that detail this process?
- nanolith 2y ago
  Not yet, but very soon. My previous work was done for employers and involves code that is not free to distribute. I am currently working on some blog articles to cover a web application written in model checked C. Once that is done, and once my personal C parser library is complete, I'll write a series of articles on constructive and equivalence proofs of software written in C. A bucket list item for me is to write a series of books on this, focusing less on the academic aspects and more on the practical aspects. There are plenty of excellent text books on this, but few "how to I write real world code that is model checked / constructively proven?" Unfortunately, this has led to a lot of odd opinions being passed around as fact, like that it takes 30 man years to write constructively proven code, or that model checking is impractical.

skulk 2y ago

> I'll use Coq or Lean to define an abstract machine model, then either extract code from this model into C, C++, or machine code, Do you have any worked examples or blog posts that detail this process?

nanolith 2y ago
Not yet, but very soon. My previous work was done for employers and involves code that is not free to distribute. I am currently working on some blog articles to cover a web application written in model checked C. Once that is done, and once my personal C parser library is complete, I'll write a series of articles on constructive and equivalence proofs of software written in C. A bucket list item for me is to write a series of books on this, focusing less on the academic aspects and more on the practical aspects. There are plenty of excellent text books on this, but few "how to I write real world code that is model checked / constructively proven?" Unfortunately, this has led to a lot of odd opinions being passed around as fact, like that it takes 30 man years to write constructively proven code, or that model checking is impractical.