First impressions of Coq and “Certified Programming with Dependent Types”

A simplistic view of strongly typed functional programming ecosystem is that the two most influential languages are Haskell and ML. Haskell is my language of choice so when it came to learning dependently-typed programming I stayed on the Haskell side of the spectrum and went with Agda and Idris. I chose the two over the ML-inspired Coq, most often advertised as a proof assistant rather that a programming language, planning to learn it “when I find some free time”. I wouldn’t probably find that time if it wasn’t for a friend of mine who recently picked up a book “Certified Programming with Dependent Types” by Adam Chlipala of MIT. Having a companion to discuss the ideas in the book was a perfect opportunity to pick it up – the truth is I found out about the book well over a year ago and since then it stayed on my always too long must-read-this-some-day list. So far I have read around 1/3rd of the book and would like to share some of my first impressions, both about the book, which I will refer to as CPDT, and Coq.

(Note: In what follows I will compare Coq to Agda and Idris but you have to be aware that despite similarity in features of these languages they don’t aim to be the same. Coq is a proof assistant with an extra feature of code extraction that allows you to turn your proofs into code – if you ever heard about “programs as proofs” this is it. Idris is a programming language with extra features that allow you to prove your code correct. I’m not really sure how to classify Agda. It is definitely on the programming-language-end of the spectrum – it allows you to prove your code correct but does not provide any extra built-in proof support. At the same time turning Agda code into working programs is non-trivial.)

Let me start off by saying that I don’t have any real-life Coq project on the horizon, so my learning is not motivated by need to solve any practical problem. My main driving force for learning Coq is purely interest in programming languages and seeing how Coq compares to Agda and Idris. A common thing with dependently-typed languages is that the types can get too complicated for the programmer to comprehend and thus a language requires an interactive mode to provide programmer with compiler feedback about the types. This is true for Agda, Idris and Coq. Agda offers a great support for holes: programmer can insert question marks into the program code and once it is re-compiled in the editor (read: Emacs) question marks become holes ie. places where Agda compiler provides user with feedback about expected types, bindings available in the hole context as well as some nice inference features allowing to automatically fill in contents of holes. So in Agda one proves by constructing terms of appropriate types. Coq is different, as it relies on a mechanism called “tactics”. Once the user writes down a type (theorem) he is presented with a set of goals to prove. Applying a tactic transforms the current goal into a different goal (or several goals). Conducting consecutive steps of the proof (ie. applying several tactics) should lead to some trivial goal that follows from definition and ends the proof. To work with Coq I decided to use Proof General, an Emacs extension for working with proofs (many other proof assistants are supported besides Coq)1. It launches Coq process in the background and essentially integrates writing code with proving. With Proof General I can easily step through my proofs to see how the goals are transformed by usage of tactics. Idris falls somewhere between Agda and Coq. As stated earlier it is mostly a programming language but it also provides tactic-based proving. So for example when I write a definition that requires explicit proof to typecheck, idris-mode launches interactive REPL in which I can conduct a proof in a fashion similar to Proof General and once I’m finished the proof is inserted into the source code. the result looks something like this:

par : (n : Nat) -> Parity n
par Z = even {n=Z}
par (S Z) = odd {n=Z}
par (S (S k)) with (par k)
  par (S (S (j + j)))     | even ?= even {n = S j}
  par (S (S (S (j + j)))) | odd  ?= odd {n = S j}
 
---------- Proofs ----------
 
Basics.par_lemma_2 = proof
  intros
  rewrite sym (plusSuccRightSucc j j)
  trivial
 
 
Basics.par_lemma_1 = proof
  intros
  rewrite sym (plusSuccRightSucc j j)
  trivial

The last time I checked Idris once the proof was completed and added to the source code it was not possible to step through it back and forth to see how goals are transformed. (Things might have changed since I last checked.)

So far I’ve been doing rather basic stuff with Coq so I haven’t seen much that wouldn’t be also possible in Agda or Idris. The biggest difference is that Coq feels a much more grown up language than any of the mentioned two. One totally new thing I learned so far is co-induction, but I’m only starting with it and won’t go into details, rather leaving it for a separate post. (Agda also supports co-induction.)

As for the CPDT book I have to say it is a challenging read: it’s very dense and focuses on more advanced Coq techniques without going into details of basics. As such it is a great demonstration of what can be done in Coq but not a good explanation of how it can be done. Depending on what you are expecting this book might or might not be what you want. As stated earlier I don’t plan on applying Coq in any project but rather want to see a demo of Coq features and possibly pick up some interesting theoretical concepts. As such CPDT works quite well for me although I am not entirely happy with not being able to fully understand some of the demonstrated techniques. As such CPDT is definitely not a self-contained read, which I believe was a conscious decision on the author’s side. Discussing with people on #coq IRC channel and reading various posts on the internet leads me to a conclusion that CPDT is a great book for people that have been using Coq for some time and want to take their skills to a new level. The main theme of the book is proof automation, that is replacing tactic-based sequential proofs with automated decision procedures adjusted to the problem at hand that can construct proofs automatically. Indeed tactic-based proofs are difficult to understand and maintain. Consider this proof of a simple property that n + 0 = n:

Theorem n_plus_O : forall (n : nat), plus n O = n.
  intros.
  induction n.
  reflexivity.
  simpl.
  rewrite IHn.
  reflexivity.
Qed.

To understand that proof one has to step through it to see how goals are transformed or have enough knowledge of Coq to know that without the need of stepping through. Throughout the book Adam Chlipala demonstrates the power of proof automation by using his tactic called crush, which feels like a magic wand since it usually ends the proof immediately (sometimes it requires some minimal guidance before it ends the proof immediately). I admit this is a bit frustrating as I don’t feel I learn anything by seeing crush applied to magically finish a proof. Like I said, a good demo of what can be done but without an explanation. The worst thing is that crush does not seem to be explained anywhere in the book so readers wanting to understand it are left on their own (well, almost on their own).

What about those of you who want to learn Coq starting from the basics? It seems like Software Foundations is the introductory book about Coq and – given that the main author is Benjamin Pierce – it looks like you can’t go wrong with this book. I am not yet sure whether I’ll dive into SF but most likely not as this would mean giving up on CPDT and for me it’s more important to get a general coverage of more advanced topics rather than in-depth treatment of basics.

  1. Other choices of interactive mode are available for Coq, for example CoqIDE shipped by default with Coq installation []

4 Responses to “First impressions of Coq and “Certified Programming with Dependent Types””

  1. Geoff says:

    Great overview of a complicated language landscape, thank you very much! I am only somewhat familiar with Agda and Idris, but I use Coq quite often in my research work. I have to say, I agree with your assessment of CPDT. I’ve watched many people try to start learning Coq from CPDT and they almost always feel baffled and overwhelmed. It’s especially confusing because the first chapters (through the part about compiling arithmetic expressions to a stack language and proving equivalence) are aimed squarely at beginners and also do a great job of motivating the approach. But from there, it goes very deep very fast. It is unfortunate imo that CPDT is the first hit for “coq programming” on Amazon, and Bertot’s equally unsuitable-for-beginners reference manual is the second. Software Foundations is by far the best introduction that I am aware of. If you give it a try, I’d like to know what you think.

  2. gasche says:

    > Indeed tactic-based proofs are difficult to understand and maintain.

    I think that perception is partly wrong. It is possible to write good proof scripts that are understandable and reasonably easy to maintain (there are pain points, but other solutions not involving tactics also have pain points). For example, using bullets to structure your script makes the proof much easier to understand:

    Theorem n_plus_O : forall (n : nat), plus n O = n.
    intros.
    { induction n.
    – reflexivity.
    – simpl.
    rewrite IHn.
    reflexivity.
    }
    Qed.

    For easy proofs, using a more compact style can also help notice the important part (use the induction hypothesis in the second case):

    Proof.
    induction n; simpl; [ | rewrite IHn ]; reflexivity.
    Qed.

    I think we should strive to make our tactics as readable as possible (but I’m fine with having to step through it to regain intuition of what it does), even if the most robust and readable way is not necessarily the first version that works. You often start in a rather exploratory style, and then move towards more robustness and better automation.

  3. Jan Stolarek says:

    Being a Coq beginner I can’t really say much from experience but it looks like your ideas here don’t actually solve the problem, only postpone it. My example was of a trivial property and it already required 4-5 tactics. I imagine that at some point proofs get quite large and understanding them really becomes hard, especially after not looking at them for some time. Actually it’s the same kind of argument that is used against imperative programming – to understand it you have to execute it in your head to see how the states change during execution. Adam’s argument that one should construct an automated way of constructing proofs for a given problem domain convinces me and really looks like the right way of doing things.

  4. marisa says:

    Your overview of CPDT is pretty accurate. I’d like to add a few more points on Coq.
    1: Coq has tactic refine which is basically agda type holes.
    2: tactic can be “debugged” by using info, so you can get in and see what it does.
    3: automation can be throw away if they are hard to maintained; Just Print what you get after QED or Defined and use what you get as the definition of function.
    4: Tactics can be made to be more readable than Codes, at least in special cases with care, as gasche says. If you insist on “no need to run it in head”, than you can do 4 or complete automation tactic such as omega, debug auto (this print what it does) and crush. That said, the power of deciding to do tactic lies in you, and it is indeed useful in atleast some cases, so I don’t think it is harmful.

Leave a Reply

(required)

Staypressed theme by Themocracy