Learn Coq in Y Minutes

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?

lexpar• 7 years ago

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...

kryptiskt• 7 years ago

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.

ouid• 7 years ago

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.

polymatter• 7 years ago

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.

goodmattg• 7 years ago

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!

topmonk• 7 years ago

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

cinnamonheart• 7 years ago

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.)

philzook7• 7 years ago

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...

ibic• 7 years ago

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

janvdberg• 7 years ago

I love learnxinyminutes.com: ad-free concise single page reference/tutorials. Such a simple idea, such great execution.

hcarvalhoalves• 7 years ago

I wonder, can I define floating point arithmetic w/ this language?

gmfawcett• 7 years ago

Yes:

https://hal.inria.fr/inria-00534854v1/document

https://xavierleroy.org/publi/floating-point-compcert.pdf

cjfd• 7 years ago

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.

philzook7• 7 years ago

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

philzook7• 7 years ago

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...

domnomnom3• 7 years ago

How do I pronounce Coq?

haolez• 7 years ago

Are there benefits in learning Coq for those who work mainly with general purpose programming?

tom_mellior2• 7 years ago

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.

seanwilson• 7 years ago

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.

philzook7• 7 years ago

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.

jhanschoo• 7 years ago

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.

darzu• 7 years ago

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.

nprateem• 7 years ago

That's what she said

dang• 7 years ago

Please don't do this here.

abeppu• 7 years ago

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?

philzook7• 7 years ago

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 :\ )

wuschel• 7 years ago

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.

alimw• 7 years ago

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

philzook7• 7 years ago

Hey neat! I wrote this tutorial. Lemme know if you have suggestions for improvement (or you can make a pull request).

hart_russell• 7 years ago

I've been learning my own version of Coq for decades now

siraben• 7 years ago

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/

kiterunner2346• 7 years ago

Ummm, so how is "Coq" pronounced?

sincerely• 7 years ago

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.

tarsinge• 7 years ago

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...

elcaminocomplex• 7 years ago

https://en.m.wiktionary.org/wiki/File:Fr-coq.ogg

Learn Coq in Y Minutes

Related Stories