Proof Engineering Survey Paper: Q(ED) & A

Recently, I had the joy of writing a 120 page survey paper on proof engineering:

Talia Ringer, Karl Palmskog, Ilya Sergey, Milos Gligoric, and Zachary Tatlock. QED at Large: A Survey of Engineering of Formally Verified Software. Foundations and Trends in Programming Languages (FTPL), Vol. 5: No. 2-3, pp 102-281, September 2019.

This was a lot of work. It took two years of reading hundreds of papers, talking to dozens of experts, writing, playing with examples, soliciting feedback, and refining. The end result was a 120-page distillation of the state of the field so far and some promising future directions.

I’ll write more about what it was like to write this paper at some point. But for now, here’s a brief Q(ED) & A for interested readers. Because you’re probably wondering, “This is cool, but where do I find it, and how the heck do I read it? 120 pages? Really?”


Q: Where can I get a copy of this paper?

A: You can purchase a copy from the publisher here. If that is not accessible to you, but you would really like to read it, please contact us directly to ask about a personal copy. There will be a delay before we host our own copy online.

Q: Is this the authoritative source of what to cite?

A: No. I mean, it’s a really, really good entry point into the area. It’s a great place to start if you are looking to cite some work in this area. But it is also non-exhaustive. So, in addition to citing the survey and whatever work you find relevant in the survey, please also check the errata to make sure that you also cite the papers that we missed, search for papers that have surfaced since the survey, and check the papers that each paper cites to make sure that you get a complete view of the area.

Q: Do I really need to read 120 pages?

A: No, of course not. Then you would miss the 60 pages of citations! Don’t forget those!

OK but really. The reading guide in Section 1.4 says it best:

It is not always necessary to understand previous chapters in order to understand later chapters; readers should feel free to skip sections or chapters, or to consult later chapters or cited resources for more information.

We recommend reading the introduction, conclusion, and any sections that interest you. We also recommend scanning the errata briefly, especially for omitted citations and factual corrections. We are flattered if you want to sit down and read every single word, but we believe it is not necessary to do so in order to benefit from the paper.

Since we aim to address a broad audience, below are some specifics beyond that for particular kinds of readers. You can obviously read this however you want, but these are just some potentially helpful strategies. If you do not fit any of these profiles, feel free to contact us directly for advice on how to approach this monolith.

The Proof Engineer

pexels-photo-1260309.jpeg

You are a proof engineer working on a large proof development. Your main goal in reading this paper is to make your life easier.

We think chapters 5, 6, and 7 are probably the meat of what will help you. You probably do not need much motivation for the problem, so Chapters 2 and 3 may not be as interesting to you as later chapters (unless you work in one of the domains from Chapter 3). Skimming Chapter 4 may help if you have a choice over which proof assistant to use, but you don’t need to get too lost in the details.

The New Researcher

pexels-photo-2529285.jpeg

You are about to embark on the exciting journey that is graduate school, or something like that. Really, you’re just looking for a cool project. You’re pretty open, but verification using interactive theorem provers sounds nice.

We think the future work sections sprinkled throughout the paper will be the most interesting to you. If I were advising a student in this situation, I would tell the student to do start by reading Chapters 1 through 4, but only at a very high level, not getting lost in details. Then, search for the keywords “beyond” and “future”; read the future work sections this brings up, and think about whether those problems sound interesting. If they do, read the relevant sections, and also check the errata for those sections. In addition, read any sections you find interesting, and read the conclusion. Supplement with any resources from Section 1.4 that you find necessary to understand the sections that deal with the problems you find most interesting.

The Concerned Researcher

pexels-photo-256548

You already know what you want to work on, but you want a good idea of related work. You hope this will help make your life easier, and you also hope it will help you write your related work section and ensure that your work is novel.

We recommend focusing on the sections most relevant to your work. Then, if you are still interested, you may wish to read more. We also recommend checking the errata before citing any papers that we cite to make sure that you also cite the papers that we missed. We recommend searching for papers that have surfaced since the survey, and also checking the papers that each paper cites to make sure that you get a complete view of the area.

The Advisor

pexels-photo-1094072

You are advising some students who are potentially interested in verification. You want a good overview of the field so that you can advise them well.

We recommend an end-to-end read, but focusing little on low-level details. Having a broad overview of the field is important, and the best way to get this will likely be to just dip your toes into every section. A more detailed read may help when you pick out a particular project. You may also want to refer your students to the paper and have them follow the advice for them in this guide.

The Tool Developer

pexels-photo-1496139.jpeg

You are developing or maintaining a proof engineering tool, or maybe even an interactive theorem prover. You want some ideas for how to improve your tool, or you just want to scope out the competition.

We—OK, Ihave strong opinions about this one, since this is the kind of research I do. You’ll want to read Chapter 3 just to get an idea of who some of your users might be. Then, you’ll want to learn the concepts necessary to communicate with tool developers from other communities; for this, read Chapter 4, Section 5.1, and Section 7.1. The Coq developers, for example, could learn a lot from the pain points the Isabelle/HOL developers have faced; the selected chapters and sections can help you speak each others’ languages. Then, of course, you can read the sections that are most relevant to the tool you are developing. But again, approach this with an open mind, considering tools from many different proof assistants. And finally, make sure you check the errata for omissions, like the HOL definitional mechanisms.

The Entrepreneur

kids-girl-pencil-drawing-159823.jpeg

You are running a business or managing a team of engineers, and you think maybe verification is worth it. You’re not sure, though. You think maybe this paper will help.

We recommend reading the introduction in detail, as well as Chapter 3 (aside from the mathematics section) for an idea of some domains in which verification has already seen success. You can probably skip Chapter 4 and Chapter 5. You will likely want to skim Chapters 6 and 7, but at a high level, without getting lost on details; these may help you understand what is currently difficult, so you can do some cost-benefit analysis. The conclusion should also be helpful for this.

The Newcomer

kid-notebook-computer-learns-159533

You have just set foot on this Earthin particular, on the world of proof engineering. You don’t really know what’s going on. Help? Oh god this is 120 pages? A nap sounds better.

We are really happy that you found this survey! Don’t panic. You really don’t need to understand everything in this survey. We honestly recommend the same strategy we recommend to The Advisor (skim the whole thing), but really, really being unafraid to skip sections that are inaccessible. Check out the resources in Section 1.4 if you really want to understand more.

Q: I found a mistake or omission. Where do I report it?

A: We will add it to the errata! Please report it as a GitHub issue or pull request modifying the errata source file, or contact us directly.

Q: How do I cite this paper?

A: Please cite the following:

@article{PGL-045,
url = {http://dx.doi.org/10.1561/2500000045},
year = {2019},
volume = {5},
journal = {Foundations and Trends® in Programming Languages},
title = {QED at Large: A Survey of Engineering of Formally Verified Software},
doi = {10.1561/2500000045},
issn = {2325-1107},
number = {2-3},
pages = {102-281},
author = {Talia Ringer and Karl Palmskog and Ilya Sergey and Milos Gligoric and Zachary Tatlock}
}

Q: Why did you write this paper?

A: Because we need new hobbies?

Also, though, the words “proof engineering” have been thrown around for a while, and we think it’s time to really define the field. We think this is a good start. We hope it will help people from many different backgrounds to get a sense of what proof engineering is, why it’s useful, and what the oustanding challenges are.

Thanks for reading our paper! Let us know what you think.


Any opinions, findings, and conclusions or recommendations expressed in this material are those of the authors and do not necessarily reflect the views of the National Science Foundation.

Advertisements

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Google photo

You are commenting using your Google account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s