Information
- Lecturer : Kalmer Apinis (kalmer.apinis@ut.ee)
- Lectures : Thursdays, 10:15-12:15, in Delta-2047
- 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 VS Code/Codium.
- Install Opam, the package manager for the OCaml programming language.
- Initialize
~/.opam. Run via terminal:
opam init eval $(opam env)
- Install Coq
opam pin add coq 8.18.2 opam install vscoq-language-server
- Install VSCodium and install the extension VsCoq
Why verified algorithms?
While many application domains require us to "move fast and break things," there are important industries, such as avionics, space, and medical devices, where such a stuck accelerator pedal approach is not desired. In this course, we will learn how software correctness guarantees are achieved through the Coq system, whose many industrial uses include the certified compiler (CompCert) used by Airbus. All of this may seem like hard work, but it will pay off, just as the focus on quality assurance has paid off for Airbus.
What is interactive theorem proving
An interactive theorem prover such as Coq is a system where you can write propositions (such as "forall l1 l2, rev (l1 ++ l2) = rev l2 ++ rev l1") and prove them interactively. Proving something interactively means that the system keeps track of your goals as you apply logic rules and proof tactics. In the background, the system checks that the rules you have chosen are applicable and prohibits you from using rules that make no sense. This means that Coq proofs are machine-checked.
Why interactive theorem provers?
As code becomes easier to generate, it is increasingly important to precisely specify, clearly understand, and thoroughly verify the correctness of our programs. Thus, tools like Coq complement tools like ChatGPT and Copilot by requiring proofs and checking that provided proofs are indeed valid. Look at our experiment, where ChatGPT generates a buggy implementation for the simple problem of finding the maximal element in a binary tree.
Is Coq the right tool?
In this course, we use the Coq system, but other similar tools exist. Coq can be used to formalize mathematics in general, but it can also be used to prove the correctness of programs. This fact makes Coq interesting for computer scientists.
Coq is not a toy or just a program that teaches students about logic. It is a mature tool with 30 years of research behind it. It is actively used 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.
In this course, we learn to write programs in Coq, prove logical propositions, and reason about small imperative and functional programs. As an added benefit, the Coq systems will provide instant feedback on whether your homework solution is correct.
Forms of learning
During the recorded lecture, I will solve the majority of exercises from Logical Foundations and Verified Functional Algorithms. These are the same exercises you must solve and submit as 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 "Verified Functional Algorithms" chapters, 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 use 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.