Hacker News Reader

Comment by paulgb | Hacker News Reader

Are there any good resources (similarly short and informal) about doing proofs in Coq? I don't have anything particular to prove, but I find it interesting and would like to build up intuition for the Curry-Howard Correspondence.

Also, more tangential, but this comment section might attract people who know the answer: any good resources for getting started on type systems more generally?

View on HN

Software Foundations (https://softwarefoundations.cis.upenn.edu) is pretty informal and understandable, what it isn't is short. But it's a very useful resource.

The best general introduction is probably still Types and Programming Languages: (https://www.cis.upenn.edu/~bcpierce/tapl/index.html) It's a great book, but it doesn't get to dependent types.

It should be mentioned that software foundations is basically a videogame that you can play in your coq interpreter. Short is less relevant than fun, imo.

I will second that Types and Programming languages is a great book. The next book, https://www.cis.upenn.edu/~bcpierce/attapl/index.html does get into Dependent Types.

I'm currently in Prof. Pierce's class at UPenn! Can confirm this is a great book, and we literally work through the exercises. Taking this class AFTER using Scala in industry has really put a lot into context. It's so easy to start too - download CoqIDE or ProofGeneral and get to it!

If you know Haskell, or are willing to learn, this is a brilliant explanation with code (you build a dependently typed language as you go). It ramps you up very fast yet each step is accessible. This alone really caused me to get bit by the dependent type bug.

https://augustss.blogspot.com/2007/10/simpler-easier-in-rece...

Here is the example code from this post

https://github.com/scott-fleischman/simpler-easier?files=1

>Also, more tangential, but this comment section might attract people who know the answer: any good resources for getting started on type systems more generally?

I like Philip Wadler's Programming Language Foundations in Agda: https://plfa.github.io/

>The original goal was to simply adapt Software Foundations, maintaining the same text but transposing the code from Coq to Agda. But it quickly became clear to me that after five years in the classroom I had my own ideas about how to present the material. They say you should never write a book unless you cannot not write the book, and I soon found that this was a book I could not not write.

I found Agda + PLFA was more approachable for me than Coq + Software Foundations.

(Edit: clarifying that I'm responding to the tangent.)

I took a graduate class where we worked though the first and second volumes of Software Foundations (https://softwarefoundations.cis.upenn.edu/). These are very nice introductions to the Coq environment and are being actively improved. The textbook is available online, with the source file of each chapter being a valid coq script, making it easy to experiment. There are also a large amount of interesting and challenging exercises.

Here's a link to the chapter on the Curry-Howard correspondence: https://softwarefoundations.cis.upenn.edu/lf-current/ProofOb...

Short and informal is hard to come by here, especially by such a formal system built by such formal people.

This tutorial maybe?

https://coq.inria.fr/tutorial-nahas

This particular chapter of Software Foundations may be helpful (or it might not be. If so don't sweat it, it isn't really meant to be read in isolation)

https://softwarefoundations.cis.upenn.edu/lf-current/ProofOb...

I found this one quite useful from the aspect of proving (I'm reading it half way): https://coq.inria.fr/tutorial-nahas

At the end of the article, there is a coq source code of the entire article for you to play with in CoqIDE or Proof General: https://mdnahas.github.io/doc/nahas_tutorial.v

Reply on news.ycombinator.com