What is interactive theorem proving
An interactive theorem prover such as Coq is a system where you can write propositions (such as "A ⋀ True → A") and prove them interactively. Proving something interactively means that the system keeps track of your goals as you apply logics rules and proof tactics. In the background, the system checks that the rules you have chosen are applicable and prohibits you to use rules that make no sense. This means that Coq proofs are machine-checked.
In this course we use the Coq system, but there are other similar tools. Coq can be used to formalize mathematics in general, but it can also be used for proving correctness of programs --- this fact makes Coq interesting for computer scientists.
Coq is not a toy or just a program that teaches students about logics. It is a mature tool that has 30 years of research behind it, which is actively used to for formalizing complicated proofs. Wikipedia lists its main achievements as
- Four color theorem: formal proof using Coq was completed in September 2004.
- Disjoint-set data structure: correctness proof in Coq was published in 2007.
- Feit–Thompson theorem: formal proof using Coq was completed in September 2012.
- CompCert: an optimizing compiler for a subset of the C programming language which is fully programmed and proved in Coq.
The main goal for this course, as the name suggests, is for you to be able to prove the correctness of some algorithms that, as a simplifying factor, are implemented functionally.
Forms of learning
During the recorded lecture, I will solve exercises from Logical Foundations and Verified Functional Algorithms. These are the same exercises that you need to solve and submit as your homework. You can choose according to your preference how closely you want to follow the lectures.
In addition to lectures, there will be a Zulip chat room for cases where you get stuck with details or understand "the big picture".
The homework will have quite strict deadlines as extra motivation to not fall behind too much.
Scope of the course
We expect that you understand programming and algorithms at a basic level. For example, you should understand what merge sort does.
No previous knowledge about proofs or Coq is needed. Some knowledge of logic and proofs will come in handy. We start at the beginning: the basics of Coq. Then we learn all required proof tactics and apply them to prove the correctness of functional algorithms such as sorting, search trees, and priority queues. I am not obsessed with covering all chapters of "Verified Functional Algorithms" but we should aim to reach Red-Black tree operations.
Motivation for taking the course
- Being able to use interactive theorem provers (including Coq) is useful. There are high-paying jobs in Europe for writing provably correct software. Also, proving something interesting is a suitable topic for your PhD. Coq might never go mainstream, but provably correct software is the future. :-)
- Surprisingly few people in Estonia are using it. Stand out among your peers with uncommon know-how/interests.
- As Coq is able to check your proofs, you get instant progress feedback on your course- and homework. By solving all the exercises in a timely manner, you are almost guaranteed to get a good result on the exam, as the exam is about proving similar theorems as homework.
- You will get a better intuition about correct algorithms.
- You will be able to write provably correct code.
Information
- Lecturer : Kalmer Apinis (kalmer.apinis@ut.ee)
- Lectures : Tue 12..14 Delta-2035; Thu 12..14 Delta 2010
- Homework : see Homework, submit to moodle
- Discussion : Zulip (log into courses to see link)
- Final exam:
- open book e-exam (including the internet) + face-to-face Q&A if needed
- example
- Final grade
- max. 70 points for autograded HW (less if incorrect or submited late)
- max. 30 points for autograded exam+Q&A
- 0..50 → F, 51..60 → E, 61..70 → D, 71..80 → C, 81..90 → B, 91..100 → A
Book recommendation
- Verified Functional Algorithms by Andrew W. Appel
- Logical Foundations by Benjamin C. Pierce et al
- "Certified Programming with Dependent Types", Adam Chlipala, 2019
- Program Logics for Certified Compilers by Andrew W. Appel et al., 2014
- Formal Reasoning About Programs by Adam Chlipala, 2017
- Computer Arithmetic and Formal Proofs by S. Boldo and G. Melquiond, 2017
- Binomial Queues by Andrew by W. Appel, 2016
- Efficient Verified Red-Black Trees by Andrew W. Appel, 2011
Preparation for the course
- We will be using Coq together with CoqIDE.
- Install Coq version 8.15.
- In Windows and OS X I suggest downloading Coq Platform from https://coq.inria.fr/download
- In Linux you can probably use a package manager.