For the first class, we will read Chapters 1 and 3 of QED at Large: A Survey of Engineering of Formally Verified Software [PDF] [DOI] by Talia Ringer, Karl Palmskog, Ilya Sergey, Milos Gligoric, and Zachary Tatlock.
QED at Large is a survey paper about engineering formally verified proofs of program correctness; Chapters 1 and 3 are background and motivation, with a focus on impacts. They should give you a sense of some cool applications of proof assistants over the last several decades.
You can find the video lightning lecture for the first class here, and the corresponding slides with notes here. You can find a reading guide and the discussion questions below. The video will be posted when it is ready.
Please note that because of POPL, this reading is not due until January 25th at 10:00 AM. From next week forward, readings will be due the morning before the corresponding class.