QED at large

Stream: general

[Mario Carneiro]

Forwarding a post from Talia Ringer on coq-club that would be interesting to readers here as well:

Hi all,

Are you stuck at home thanks to a pandemic? (Same.) Good news! We've made our proof engineering survey paper "QED at Large: A Survey of Engineering of Formally Verified Software" available for free on arXiv. You can find it at this link.

It's over 120 pages without citations, so it should keep you occupied for a bit. If you're not quite sure where to start, check out our Q&A and reading guide.

Of course, be sure to check the errata for the mistakes and omissions we've identified and corrected since the original publication. Instructions for suggesting new corrections and omissions are on the errata website. The version above has the same content as the journal version. We do plan to integrate corrections from the errata at some point for later versions.

Stay healthy and enjoy the read! Thanks again to everyone who gave us feedback while we were working on the original version, and to everyone who has given us feedback for our errata!

Talia