Information
- Lecturer : Kalmer Apinis (kalmer.apinis@ut.ee)
- Practicals : every Monday, 14:15 .. 16:00, r512
- Homework : every other week (~7 times), pass/fail, repeated/late submissions allowed
- Final exam:
- On May 23rd, 14:15 .. 16:00, room 512
- all homework must be passed before
- open book exam (including the internet)
- ~80% proving theorems, ~20% short questions
- 0..50 → F, 51..60 → E, 61..70 → D, 71..80 → C, 81..90 → B, 91..100 → A
- More in Moodle
Book recommendation
Preparation for the course
- We will be using Coq together with CoqIDE.
- Install either version 8.14 or 8.15.
- In Windows and OS X I suggest downloading CoqIDE from https://coq.inria.fr/download
- In Linux you can probably use a package manager.
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. (Although we are not focusing on that fact in this course, as it would make it more difficult to learn the basics.)
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.
Difficulty level of the course
The reason that proving is complicated in general is because it requires complicated combination of rules. All rules are simple by themselves. As we do not look at statements that require large proofs, everything in this course should be fairly simple. In my opinion, this is very important for the introduction --- you need to understand the basics and experience that it is simple enough.
In this course, we are going to prove a large number of rather simple statements. Real-world proofs just require you to break up complicated proofs into simple ones.
Motivation for taking the course
- Being able to use interactive theorem provers (including Coq) is useful. There are highly 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 an uncommon know-how/interests.
- The course is very accessible compared to similar courses in other universities in the sense that it does not require expert knowledge of logics, type theory etc. This course is suitable for Bachelor students.
- As Coq is able to check your proofs, you get instant progress feedback on your course- and home-work. By solving all the exercises given in the practical sessions, you are almost guaranteed to get a good result on the exam, as 80% of the exam is proving similar theorems as in the practicals.
If it sounds interesting to you then there is no reason not to take the course. Just register and see if it suitable/interesting to you in the end.