Learn Coq in Y Minutes
learnxinyminutes.com
learnxinyminutes.com
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?
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.
https://augustss.blogspot.com/2007/10/simpler-easier-in-rece...
Here is the example code from this post
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.)
Here's a link to the chapter on the Curry-Howard correspondence: https://softwarefoundations.cis.upenn.edu/lf-current/ProofOb...
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...
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
And the symbol : https://en.m.wikipedia.org/wiki/Gallic_rooster
For example, the idea of strengthening & weakening the inputs/outputs of your lemmas, functions, or any abstraction is really central Coq. Constantly there is a tension between weakening your preconditions so your abstraction is easier to apply while also strengthening your postconditions so you get more leverage from you abstraction, or doing just the opposite so that implementing the abstraction is possible.
After working with Coq almost exclusively for a year and then returning to regular programming, I find this is a concept I come back to constantly.
It applies to any language. One example is creating library API preconditions & postconditions such that the API is useful to the caller but not so tight that there's no room to change implementation details as the maintainer. With API contracts in particular, it's usually possible to strengthen a postcondition and weaken a precondition without breaking compatibility so it's helpful to start with weaker postconditions and stronger preconditions to give you that flexibility.
In regular languages, preconditions & postconditions is something that the language only helps you out partially. Even in Haskel this is true. Most of the contract is not enforced by the type system and can only be described in documentation. If your API takes in a "number", chances are there are bounds on what that number can be, e.g. non-negative or less than the length of the list. In Coq, all of this would be very explicit and machine enforced. When writing contracts now, I sometimes imagine what lemmas and witnesses I would have written or assumed in Coq and that helps me think about the trade offs.
This concept often applies beyond APIs to the whole system architecture. What should that microservice require of its inputs and what guarantees can that storage system provide, etc.
If you have a concurrent program you can also try encoding a fragment with simplified semantics in Coq and prove the correctness of the program in Coq.
https://softwarefoundations.cis.upenn.edu/current/plf-curren...
Here is an example of that for a toy language.
If you find it hard to justify robustly in your head why some code should work it's probably very difficult to prove formally which usually means there's a large surface area for bugs too.
I found a big aspect of proving program correctness was formulating programs in a way first that made them easier to prove. It makes you cringe at mutable state and loops with nontrivial conditions.
I think it's really interesting though, so it doesn't hurt to give it a looksy.
[1] https://softwarefoundations.cis.upenn.edu/lf-current/index.h...
>Did you really need to name it like that?
>Some French computer scientists have a tradition of naming their software as animal species: Caml, Elan, Foc or Phox are examples of this tacit convention. In French, “coq” means rooster, and it sounds like the initials of the Calculus of Constructions CoC on which it is based.
https://www.elsevier.com/books/computer-arithmetic-and-forma...
You may also want to look at this thesis