CS 3820, Spring 2020: Recent Episodes
Aaron Stump
Some lecture materials from CS 3820, "Programming Language Concepts", at The University of Iowa Spring 2020. I am posting these as part of taking my class virtual due to the COVID-19 pandemic. The part of the class covered is mostly on Agda.
Internal verification is an approach where the proof of some property of a piece of code is layered on top of that code. Instead of having 2 artifacts -- code and proof -- we just have one, namely this composite of code and proof. The advantage is that a lot of the time the proof can piggyback on the code, when the two share their recursive structure (which is pretty often). Discussion of these ideas.
The Curry-Howard isomorphism identifies induction and terminating recursion. To prove a property by induction, one just writes a terminating recursive function. This episode introduces these ideas in more detail.
This episode is about Chapter 2 of the Agda book. Agda is based on the Curry-Howard isomorphism, which identifies typed (pure) functional programs and constructive proofs. In this episode, I introduce the idea of the Curry-Howard isomorphism, and constructive versus classical reasoning.
In this episode I discuss the amazing idea of doing mathematical proofs about our software, and contrast it to other methods for ensuring code quality, like testing or code reviews. I also start talking about Agda, in particular some of the differences we will see from coding in Haskell, despite a lot of connections between Agda and Haskell.