Lecture preparation

Before lecture, read the paper assigned below, and submit two items to the submission website:

Also keep in mind that you will need to write a paper summary for your choice of papers throughout the semester.


Read the paper IronFleet: Proving Practical Distributed Systems Correct by Hawblitzel et al.

Why are we reading this paper?

What to learn from this paper?

Answer this question

In the IronFleet paper, what is the spec for an overall system, what is the code that they prove meets the spec, and what is the sequence of arguments (e.g., different types of refinement) that the authors use in their proof? Which of these proof arguments are machine-checked, and which are done on paper?