Roadmap

Status Quo

After having completed the Guru book I did a brief and shallow survey of the field to see what to learn next. To skip to the chase, I will currently focus on learning Agda next. If you are interested in why, then continue reading as I briefly discuss some alternatives that I did not choose for now. Please be aware that my experience with the following is slim to none so my opinions could change drastically in the future. The plan is to invest in learning Agda now, then come back to read more general Curry-Howard and proofs-as-programs books later while transcribing examples to Agda for greater understanding. I have also spent a bit of time working on a toy implementation of the declarative Oz kernel language for elementary experience in language construction in case I feel an itch to move in that direction. I will come back to this from time to time for a small change of pace.

Agda

What’s nice about Agda is that it feels like a very natural extension of Haskell. Haskell got a lot of things right in the way of mutation-restriction via monads and powerful type inferencing. Although it recently added Generalised Algebraic Data Types they are still not as flexible as completely dependent types. Agda on the other hand fills this role quite well, in fact it is itself implemented in Haskell and even makes code sharing possible. To be fair, most proof-based languages are implemented in an ML dialect or Haskell, in contrast to the C/C++/Java dna of more traditional languages. I like Agda right now for two reasons: First it has a strong emphasis of purely functional code which is much more pleasant to deal for learning. And secondly it deals with manipulating raw proofs directly rather than using “script” abstractions. It may turn out that both of these advantages disappear after I get passed the learning stages of this field, but from briefly looking over the language it seems cohesive enough to still be practical even after learning… And a third more selfish reason is that Agda comes with a very fun Emacs mode =) My first focus will be going through this Agda course available online.

Coq

Coq is one of the older (but still actively developed) and more mature proof languages / systems. There is a well-organized Software Foundations course based on Coq available, as well as an ICFP video explaining its background… these are both by Benjamin Pierce of TAPL fame. Unlike Agda, in Coq one uses tactics to write “proof scripts” for proving. These are a higher-level abstraction than bare-bones equational reasoning. Although this sounds great in principle, like I already said I’d rather dabble at a lower level right now because I think it may result in a better base for learning. Coq also has much more literature in doing imperative proofs that I’d like to steer clear from. Either way, once I have a better foundation with Agda I will definitely revisit the course linked above to mirror exercises in it. Coq is one of those widespread languages that you cannot afford to not learn. Well… at least widespread in this community =)

Epigram

I have not dug much into this language. However I do know that is also written in and similar to Haskell, and the most comparable to Agda. A new significantly improved version of Epigram is in the works, which can be tracked at this developer blog. In fact, all of the languages in this post are still in very active development, for example check out the notes for the recent Agda developers annual meeting.

Twelf

Curry-Howard, Martin-Löf, and the calculus of constructions are all very cool ways of brilliantly relating standard programming to proofs. That being said, Twelf uses LF to take things one step further. Syntax comes as a third player to the field, making for a very unifying and grand theory. Yes… even something as unassuming as syntax stands on level ground with standard programming and proofs via things like Higher-Order Abstract Syntax… therein you can call syntax as if it were a function to perform variable substitution and eliminate a large class of variable capture problems… amazing!!! You can find a great video and mini-course about Twelf… it was part of a recently held summer school made available for free including course materials and videos (many other similar topics are covered, of course including Coq). The Twelf lectures are presented by Robert Harper of CMU so hold on to the railings for an exciting roller-coaster ride. Dr. Harper is also offering what looks like a great programming languages (in-progress) book draft for free. I will come back to Twelf later with the most excitement, mainly due to the fact that its intent is to focus on proving about formal properties of languages rather than integrated proofs for general-purpose programming. I haven’t dug in enough to know if this is just what Twelf has been used for historically or if there is some limitation. Another reason for saving this for later is that I need enough mental energy to focus on just learning on an isomorphism =p

Conclusion

So there’s my roadmap, full of fun links and hopefully a reasonable approach to diving into the exciting field of theorem proving. To summarize, the plan is to first learn Agda and then move on to more theoretical books, and finally come back to go through Coq and Twelf courses to compare each additional language I acquire knowledge about with the previous ones. Although I wasn’t expecting it, there is plenty of approachable information available. That means there are no excuses to not to explore this stuff, so join me if you would like =) As always, during the course of my learning I may find reasons to change the order I outlined above, so no promises about that. I should also note that I may dabble with going through and reworking some of the Real World Haskell book as I am learning Agda. Finally, please be kind and leave any good resources you may know of in the comments.

larrλtheliquid -> Lemma the Ultimate