I recently read the free book Software Foundations by Benjamin Pierce. The book starts by introducing basic proof theory and logic. In later chapters programming language topics like Hoare logic and type systems are taught. The Coq Proof Assistant is used in all examples and exercises in the book. In fact, the whole book consists entirely of Coq scripts written in a literate programming style.
Part of my motivation for reading the book was to learn how to use Coq. By solving all the examples I now feel pretty confident in using Coq to construct proofs for simple theorems.
Since this was the first time I have used a proof assistant, I thought I would share my thoughts about learning Coq.
It took me a long time to learn how to use Coq efficiently. The exercises in Software Foundations do a great job of introducing one small concept at a time and then practicing it in many different ways. The exercises do take a long time to solve, but I thought it was very fun to solve them. Each exercise consists of proving a theorem. It feels extremely rewarding to finally complete a difficult proof that took a long time to solve.
I got addicted to solving Coq exercises. Some exercises took me more than a week to solve. Some exercises kept me up late at night, because I could not stop thinking about them. To me it seemed like solving Coq exercises was very similar to solving puzzles in The Witness. The kick I got out of solving an exercise was very similar to the kick I got out of solving puzzles in The Witness, or other puzzle games.
The term “Proof Assistant” is deceptive. You get no assistance in figuring out how to prove properties by using Coq, however the tool assists you in checking that the proof is correct. This can be a huge help because you can be sure that you have not made a mistake, that the proof really proves what the theorem states. When I write an informal proof I always worry that I might have made a simple mistake that is not apparent to myself on inspection. This worry is erased almost entirely when using Coq. Instead, you only really have to check the theorem to see that the property being proven is actually the one you wanted to prove.
When I got deep into working on a proof, I sometimes lost track of what I was trying to prove, and how the particular subproof I was working on related to the overall theorem. It was very useful to sometimes take a break and try to think through everything from the high-level theorem again. Sometimes it was very useful to illustrate small examples on paper.
One of the exercises in Software Foundations that I found most difficult was the exercise to prove the pigeonhole principle. I was very happy with my proof when I finally completed it, so I tidied it up and published the proof on GitHub. My solution does not use the principle of the excluded middle, which is much more difficult than the version you have to prove in the original exercise.
Part of learning Coq is to learn the programming language used to write proofs. The language, Gallina, is a very advanced dependently typed functional programming language. Most concepts are familiar if you have already programmed in a functional language, which I had. The part I had most difficulty with was the way inductively defined types are declared and used in induction and case analysis.
Some aspects of functional programming can be very difficult to work with if you are mainly used to imperative programming languages. The exercises on church numerals were the most difficult for me.
I was not confident in my ability to write mathematical proofs before reading Software Foundations. I am now much more confident that I can prove simple theorems. I think this is mainly due to working through the exercises in the first six chapters of the book. These chapters introduce general techniques used to construct proofs.
The most important concepts in mathematical proofs are direct proof, case analysis, and induction. I had learned a bit about these concepts from my undergraduate studies, but I developed a much more systematic way of using them by working through the exercises in the intro chapters of Software Foundations.
The later parts of the book become very advanced, but it was easier to work through the exercises after becoming familiar with Coq.
After the introduction to proof theory, logic, and functional programming, Software Foundations continues on to Hoare logic and type systems. Some of the exercises are about proving that simple programs work according to some specification. A system for constructing such proofs in a systematic manner is introduced in the Hoare logic chapters. The chapters on type systems are all about proving that a well-typed program always makes progress (does not crash).
This was the first time I have read about type systems and Hoare logic. The book seemed to give a good introduction to these topics. I really enjoyed the exercises that were about constructing correctness proofs for simple programs.
The best thing about the book is that all the exercises can be run in interactive mode in the Coq IDE, to see how everything works. This made it fun to read the chapters about type systems.