4 ms·

> 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 examp

• 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.