Learn Coq in Y Minutes(learnxinyminutes.com)
learnxinyminutes.com
Learn Coq in Y Minutes
https://learnxinyminutes.com/docs/coq
60 comments
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.
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.
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!
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.
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.
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
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 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...
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...
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
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
I love learnxinyminutes.com: ad-free concise single page reference/tutorials. Such a simple idea, such great execution.
If you wonder about the name : https://fr.m.wikipedia.org/wiki/Coq
And the symbol : https://en.m.wikipedia.org/wiki/Gallic_rooster
And the symbol : https://en.m.wikipedia.org/wiki/Gallic_rooster
Hey neat! I wrote this tutorial. Lemme know if you have suggestions for improvement (or you can make a pull request).
Can anyone here comment on what kinds of proofs coq is a good tool for, and what kinds of proofs are impractically hard for it to handle? I'm aware that most proofs aren't formalized, and now and again we hear that mathematicians spend a long time trying to assess whether a proof has errors. From that, I infer that there are proof approaches that are challenging to capture in tools like this (or else any proof not obviously correct could be formalised to resolve the issue). What are those hard-to-capture techniques?
You may be interested in a recent survey "QED at Large: A Survey of Engineering of Formally Verified Software" https://www.nowpublishers.com/article/Details/PGL-045
(have to sign up for a free account to access :\ )
Hi, signed up for a free account, but access was not granted. Email is in my profile, if you would be so kind to help.
The big limitation of Coq is a limitation common to all proof assistants. It takes a lot of time and effort to formalise even simple mathematical ideas, so complex ones can seem quite beyond reach. However if a proof requires the analysis of more cases than a human could comfortably handle, as in the four colour theorem or the Kepler conjecture, then it is a good candidate. https://en.wikipedia.org/wiki/Proof_by_exhaustion
Are there benefits in learning Coq for those who work mainly with general purpose programming?
IMO, yes. Similar to the benefits of learning Haskel as a Javascript programmer, there are ideas better embodied in Coq that translate to all languages.
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.
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 aren't doing formal verification of programs, the other main use case of Coq would be using it to assist with coining a new domain-specific language, and proving that the language meets certain requirements.
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 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.
It's fun, and it gives you new perspectives about how you might reason about program correctness in other languages as well, even if only informally in your head.
Agree with that - I found it makes you write simpler code because you start thinking e.g. "hmm, if I write the algorithm this way, it would take forever to prove correct in Coq so it must be an overly complex approach".
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.
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.
It is fun and useful if you're interested in formal program correctness or mathematics. Maybe it's a useful bitter pill to swallow even if you're not, but the world is a wide and wonderful place, and maybe Coq isn't the best use of your time.
I think it's really interesting though, so it doesn't hurt to give it a looksy.
I think it's really interesting though, so it doesn't hurt to give it a looksy.
If you're looking to do some dependently-typed programming and theorem proving, Coq is perhaps the most mature tool to learn. It's actually two different languages, Gallina, which is what is shown in OP, and Ltac, which is the tactic language. I enjoyed Software Foundations[1], which, if you have the time, lets you self-study theorem proving starting from scratch. Somewhat less known is the book Formal Reasoning About Programs[2] which is more advanced but informative as well.
[1] https://softwarefoundations.cis.upenn.edu/lf-current/index.h...
[2] http://adam.chlipala.net/frap/
[1] https://softwarefoundations.cis.upenn.edu/lf-current/index.h...
[2] http://adam.chlipala.net/frap/
Ummm, so how is "Coq" pronounced?
https://github.com/coq/coq/wiki/Presentation
>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.
>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.
The big irony is: "Coq" is for English speaker exactly what "Bit" is in French. No problem when written, and ok spoken between grown up professionals obviously (though I still avoid translating bitwise operator because it becomes "cock to cock operator" when spoken), but elementary school with all the 8/16/32 bits consoles was painful...
I wonder, can I define floating point arithmetic w/ this language?
As others have mentioned, it's possible and has been done in the FlocQ library. I don't have personal experience using them. I would expect proving properties to be somewhat challenging. There is a book available
https://www.elsevier.com/books/computer-arithmetic-and-forma...
You may also want to look at this thesis
https://www.lri.fr/~melquion/doc/19-hdr.pdf
https://www.elsevier.com/books/computer-arithmetic-and-forma...
You may also want to look at this thesis
https://www.lri.fr/~melquion/doc/19-hdr.pdf
As a side note, I believe native floating point operations are in the works. This is more of a speed benefit though? http://drops.dagstuhl.de/opus/volltexte/2019/11062/pdf/LIPIc...
Of course. You can define more or less anything in this language. And, actually, someone has already done exactly that. See http://flocq.gforge.inria.fr/ . Never used it myself so I do not know whether it is any good.
What a great name
I've heard a completely unverified, probably untrue story that it is the French's revenge for the word "bit", which translates crudely.
Presumably its pronounced cock?
It's pronounced like the French word "coq": https://forvo.com/word/coq/#fr (because it is the French word "coq")
In brazilian portuguese cock means "galo", it's the same animal so no surprise to me here.
bitfhacker(1)
LessDmesg(3)
I've been learning my own version of Coq for decades now
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?