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?
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!
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.
>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 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.
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)
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 :\ )
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
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.
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.
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.
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.
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.
>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...
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
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.
Actually, there are binary numbers in the coq standard library. N is in the library NArith and Z is in the library ZArith. Both are binary.
Coq is not meant to be a language for computation. If you only use natural numbers to state properties like forall a b: nat, a + b = b + a there is nothing to unfold about them and no need to worry about inefficient computation.
There is an obvious equivalence between unary numbers and binary numbers. Should be quite easy to support inductive proofs with unary numbers while supporting computation with binary numbers, and simply translate between them depending on what context one is in. In fact, I believe this is what Coq does behind the scenes.
Unary numbers have a nice inductive definition with a base case, which makes them very easy to use for proofs. And as they are used heavily in the foundations of math they will be present when you are implementing any current fields in math. And you can always convert them to binary numbers at runtime if you want performance.
It's not about performance. Unary numbers are extremely cumbersome and confusing for proofs, because people are used to working with integers using arithmetic, not pattern matching. "x + 5" is infinitely better than "Succ(Succ(Succ(Succ(Succ(x)))))“. I suspect that dependently-typed languages will get at least a 50% boost in mindshare once they ditch the unary and rewrite the tutorials with regular numbers.
Please look at the OP. Notice the arithmetic expressions such as "Compute 3 + 4.", which returns "7 : nat" instead of a string of Succ applications to some Zero.
You're arguing against a problem that doesn't exist. Coq is fully capable of understanding decimal arithmetic. The fact that it uses a unary representation in proofs is not a burden that the user has to bear. (It's still a property that they can exploit of course, e.g. in inductive proofs.)
Have you actually done any proofs in one of these systems? (or used one?)
Natural numbers are used because of the induction principle you get: it's very useful, and generally straightforward to use in lots of contexts (e.g., just the other day I had students proving the correctness of multiplication implemented as iterated addition; the multiplication is over integers, but the inner loop is after you've ensured what you are iterating is non-negative, since you decrement each iteration, and _proving_ it is much more straightforward if you interpret the loop counter as a natural number).
And your point about syntax is also baffling: Coq will display natural numbers as decimal literals, not "S(S(S...".
>Unary numbers are extremely cumbersome and confusing for proofs, because people are used to working with integers using arithmetic, not pattern matching. "x + 5" is infinitely better than "Succ(Succ(Succ(Succ(Succ(x)))))“.
Have you ever written a proof using decimal numbers? Unary numbers (Peano numbers) only have two cases to match on: Z and Succ. Decimal numbers have at least ten. Even writing proofs for binary numbers in Coq is much more cumbersome than proving things about unary numbers.
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?