1. 19

The author writes:

“This is the web site for a textbook about practical engineering with the Coq proof assistant. The focus is on building programs with proofs of correctness, using dependent types and scripted proof automation.

“I’m following an unusual philosophy in this book, so it may be of interest even to long-time Coq users. At the same time, I hope that it provides an easier introduction for newcomers, since short and automated proofs are the starting point, rather than an advanced topic.”

So I’ve been looking for some kind of accessible guide to programming with dependent types, because I’ve found the existing ATS, Isabelle/HOL, and Coq introductions completely impenetrable. From my glances at the first chapters of this book, though, it seems pretty understandable. Has anyone else read it?

  1.  

  2. 14

    This was how I learned Coq. I read this book knowing Haskell well and that’s about it; I had no formal education in computer science let alone type theory and while some parts where rough I did manage to get through it.

    The whole book is a literate program which is wonderful for monkeying with bits and pieces of the examples without having to copy paste things.

    Some things to watch out for

    1. Skipping stuff comes back to haunt you with Coq, make sure you understand everything well before moving on to the next concept
    2. stackoverflow’s Coq tag is pretty lonely, but coq-club is a very friendly mailing list which is extremely active (and frequented by the author)
    3. Coq’s minor versions are not very minor, especially when it comes to tactics. Be sure to check that you’re using correct versions of Coq for the book if you want to build it.
    4. Coq’s error message are absolutely horrible, so it takes a bit of patience to understand what you’re doing
    5. Coq will try to trick you into using more advanced features, Setoids, type classes, modules, etc. Don’t bother with them until you understand CPDT
    6. A little theory get’s you a long ways with dependent types. Reading Lof’s original paper on LF is enough theory to understand quite a bit of CiC (Coq’s underlying metatheory)
    7. Use emacs. I was a vim user and I really did try to use Vim, and failing that CoqIDE but neither of them come close to working on par with Proof General + Emacs. Use evil if you have to but it is worth the switch IMO. If you can stick through it though, it’s a very rewarding experience.
    8. You cannot jump to Coq or similar without attempting at least some typed functional programming. Learning SML, Haskell, OCaml or similar is just a must if you want to understand Coq.
    1. 4

      On a side note, coqdoc is one of my favourite literate programming tools. I like how little work it takes to produce a well documented source listing; when I’m exploring a new topic, I like to create a notebook where notes are interspersed with full source listings. I often print them out and get away from the computer to read them and think over what I’ve been learning or exploring. Maybe I just haven’t found the right way to invoke haddock or ocamldoc, but I really like having the option to have the source code itself in the documentation.

      1. 3

        Thank you for all the advice! This is awesome! My only functional programming so far has been an interpreter or two in OCaml, unless you count things like Ur-Scheme.

      2. 9

        I started reading it a week or two ago, it’s been pretty accessible. It’s a much better fit for my learning style than Software Foundations was.

        1. 4
          1. 2

            The one and the same!

          2. 4

            I have a friend who said the same, and we both initially learned Coq through Software Foundations.

            1. 3

              I found the interactive style of SF more instructive. But then I did CPDT back when it had exercises, which were pretty hard compared to SF.

            2. 5

              I started reading it but soon I found myself feeling overwhelmed and not very comfortable using the crush tactic for everything; I really wanted to learn coq, so I step back and started Software Foundations (which seems to be getting some hate … do you find it too slow / “out-of-focus”?). I’m 2 chapters away of the “real juice”.

              Anyone interested in building a little community for coq learning? I just found out about coq-club, how good is it for noobs?

              1. 4

                I personally found that CPDT was a good companion book to SF. I believe Chlipala is completely correct that spending too much time in the details of proving obscures some important larger components. On the other hand, ignoring tactics (or even direct style proofs) will hinder you ability to understand how the language does what it does.

                So, I think taking a look at both together is a good way of accessing both sides of the material.

                1. 2

                  I struggled in SF because, while I was learning the tactics, I had a hard time expressing the problems I wanted to solve (i.e., it was useful for me to learn the language first and basic approaches to programming in Coq first). I just chose to switch which book I’d read first, I’ll read SF once I’m done with CPDT.

                  1. 2

                    I find SF is better if you really focus on what these proofs indicate about foundations. Conflating teaching Coq is a misfortunate but likely necessary flaw.

                2. 2

                  It’s pretty tolerant, at worst you will get a reference to SF or CPDT with a relevant section to read.