7 ms·
Learn Coq in Y Minutes
- jannes 7y agoWhat a great name
- g4d 7y agoPresumably its pronounced cock?
- tom_mellior 7y agoIt's pronounced like the French word "coq": https://forvo.com/word/coq/#fr https://forvo.com/word/coq/#fr (because it is the French word "coq")
- enz 7y agoIn French, yes.
- lsferreira42 7y agoIn brazilian portuguese cock means "galo", it's the same animal so no surprise to me here.
- bitfhacker 7y agoWith this name we should expect a great performance!
- dang 7y agoPlease don't do this here.
- philzook 7y agoI've heard a completely unverified, probably untrue story that it is the French's revenge for the word "bit", which translates crudely.
- leqnl 7y agosuq my coq Yes, I'm dismissing an entire language because its name is rubbish. Next!
- jamisteven 7y agoGonna throw this on my resume just to see the smirks on the other end of the interview table when they get to that section. "Coq SME..."
- maelito 7y agoIf you wonder about the name : https://fr.m.wikipedia.org/wiki/Coq https://fr.m.wikipedia.org/wiki/Coq And the symbol : https://en.m.wikipedia.org/wiki/Gallic_rooster https://en.m.wikipedia.org/wiki/Gallic_rooster
- LessDmesg 7y agoWhat always puzzled me is why any of these dependent type people continue using unary numbers, even at the type level. Unary numbers are a surefire way to show that a programming language is utterly impractical and its authors are noobs. Is it really that hard to embed decimal numbers with integral arithmetic to the type level instead of permanently Succ'ing the Coq?
- kryptiskt 7y agoUnary 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.
- LessDmesg 7y agoIt'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.
- gmfawcett 7y agoPlease 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.)
- dbpatterson 7y agoHave 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...".
- paulgb 7y agoAre 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 7y agoI took a graduate class where we worked though the first and second volumes of Software Foundations (https://softwarefoundations.cis.upenn.edu/ 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/ProofObjects.html https://softwarefoundations.cis.upenn.edu/lf-current/ProofOb...
- kryptiskt 7y agoSoftware Foundations (https://softwarefoundations.cis.upenn.edu 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 https://www.cis.upenn.edu/~bcpierce/tapl/index.html) It's a great book, but it doesn't get to dependent types.
- ouid 7y agoIt 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 7y agoI will second that Types and Programming languages is a great book. The next book, https://www.cis.upenn.edu/~bcpierce/attapl/index.html https://www.cis.upenn.edu/~bcpierce/attapl/index.html does get into Dependent Types.
- janvdberg 7y agoI love learnxinyminutes.com: ad-free concise single page reference/tutorials. Such a simple idea, such great execution.
- hcarvalhoalves 7y agoI wonder, can I define floating point arithmetic w/ this language?
- gmfawcett 7y agoYes: https://hal.inria.fr/inria-00534854v1/document https://hal.inria.fr/inria-00534854v1/document https://xavierleroy.org/publi/floating-point-compcert.pdf https://xavierleroy.org/publi/floating-point-compcert.pdf
- cjfd 7y agoOf 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/ http://flocq.gforge.inria.fr/ . Never used it myself so I do not know whether it is any good.
- philzook 7y agoAs 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-formal-proofs/boldo/978-1-78548-112-3 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.lri.fr/~melquion/doc/19-hdr.pdf
- philzook 7y agoAs 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/LIPIcs-ITP-2019-7.pdf http://drops.dagstuhl.de/opus/volltexte/2019/11062/pdf/LIPIc...
- domnomnom 7y agoHow do I pronounce Coq?
- deleted 7y ago[deleted]
- haolez 7y agoAre there benefits in learning Coq for those who work mainly with general purpose programming?
- tom_mellior 7y agoIt'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 7y agoAgree 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.
- philzook 7y agoIt 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 7y agoIf 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-current/Smallstep.html https://softwarefoundations.cis.upenn.edu/current/plf-curren... Here is an example of that for a toy language.
- nprateem 7y agoThat's what she said
- dang 7y agoPlease don't do this here.
- abeppu 7y agoCan 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?
- philzook 7y agoYou 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 https://www.nowpublishers.com/article/Details/PGL-045 (have to sign up for a free account to access :\ )
- wuschel 7y agoHi, 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 7y agoThe 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 https://en.wikipedia.org/wiki/Proof_by_exhaustion
- philzook 7y agoHey neat! I wrote this tutorial. Lemme know if you have suggestions for improvement (or you can make a pull request).
- hart_russell 7y agoI've been learning my own version of Coq for decades now
- siraben 7y agoIf 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.html https://softwarefoundations.cis.upenn.edu/lf-current/index.h... [2] http://adam.chlipala.net/frap/ http://adam.chlipala.net/frap/
- kiterunner2346 7y agoUmmm, so how is "Coq" pronounced?
- sincerely 7y agohttps://github.com/coq/coq/wiki/Presentation 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 7y agoThe 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 7y agohttps://en.m.wiktionary.org/wiki/File:Fr-coq.ogg https://en.m.wiktionary.org/wiki/File:Fr-coq.ogg