1. 22

From the introduction:

These are the extended notes for the INF551 course which I taught at ÉcolePolytechnique starting from 2019. The goal is to give a first introduction to theCurry-Howard correspondence between programs and proofs, from a theoreticalprogrammer’s perspective: we want to understand the theory behind logic andprogramming languages, but also to write concrete programs (in OCaml) andproofs (in Agda). Although most of the material is self-contained, the reader issupposed to be already acquainted with logic and programming.


  2. 7

    Would love to see folks who know more compare and contrast this with series like Software Foundations.

    1. 4

      I took a look at the table of contents and the summary, and here are some things I found.

      • At a high level, Software Foundations is more “consistent” in its programming languages. Both functional programming (data types, functions, and the like) and formal proofs (dependent types, Curry-Howard, and so on), are presented in Coq. This makes it easier, in my opinion, to transition from one to the other. On the other hand, the book in the OP presents OCaml (a much more well known, but not dependently typed language), and follows up with Agda, which is dependently typed. I find this a little awkward; consider this[1] quote from chapter 1 of Program = Proof.
      • Program = Proof seems to be a lot more focused on PL theory than at least Logical Foundations. While LF takes its time to get rolling with Coq and its theorem proving facilities, in P=P things like inference rules, type systems and operational semantics are presented as early as the first chapter.
      • Software Foundations is very much a guided workbook. The entire book is written as comments in a Coq source file, each sample proof can be stepped through step-by-step, and most exercises are automatically validated by Coq’s type checker. Personally, I really enjoy this; I spent a large portion of my sophomore year of college working through the problems - it felt like a puzzle game!
      • A superficial difference is that Coq has a tactic language, while Agda does not. This means that the styles of proofs in the two languages differ - in Coq, you use predefined commands, like induction, destruct, assumption, and the like to construct your proof objects. On the other hand, in Agda, you construct your proof objects from scratch, relying on the first principles of the Curry-Howard isomorphism. I think that, although Coq’s tactics are more convenient, manually writing proofs like you would in Agda can demystify the representation of proofs in dependently typed languages. As such, it may be better for a first introduction.
      • A portion of Logical Foundations (SF volume 1) and a sizeable chunk of Programming Language Foundations (SF volume 2) deal with imperative programs. This leads PLF to present and discuss Hoare logic. On the other hand, P=P seems to concern itself primarily with functional programs, especially the lambda calculus. Of course, you do get lambda calculus in PLF, but not before (if you follow the predefined reading order) the imperative programs portion.
      • If you consider all the volumes of Software Foundations, then I think its scope is much greater. Volumes 1 and 2 present material for programming languages (especially PLT), while others deal with topics like verified functional algorithms, or the validation of existing imperative programs, and property based testing. I saw a draft of an SF-like Coq book regarding separation logic, too. In this sense, it could be thought of more as a Coq cookbook.

      Aside from Software Foundations and Program = Proof, there’s also Programming Language Foundations in Agda.


      This correspondence has some limitations due to the fact that OCaml is, after all, a language designed to do programming, not logic

      1. 2

        This is fantastic and a better comparison than I could have reasonably dreamed of, let alone asked for. Thanks so much!

        1. 2

          Thank you for the great writeup! I’m currently working through Programming Language Foundations in Agda and strongly agree with your description of proof writing as like a puzzle game. I plan to read P=P after PLFA specifically because it gets into cubical agda and HoTT. Have you studied HoTT?

          1. 1

            I have not studied HoTT; as things stand, I think it’s probably above my level. I meant to write a note in my comparison about HoTT and cubical agda (I did spot them in the table of contents!), but I guess I kind of ran out of steam. I hope you enjoy reading the two books, they look like great resources!