9 ms·
Coq 8.6 is out
- iagooar 10y agoIs there a good book about more advanced usage of coq?
- Others 10y agoThat's not surprising, since that's the correct way to pronounce it...
- hawkice 10y agoIt's not homophonic with Coke? EDIT: Inria is French (although Google translate insists the less fortunate homophone still exists in French).
- nickpsecurity 10y agoThat's how I pronounce it haha. Or I say "the INRIA prover."
- theoh 10y agoWait till the GGP hears about the CoqHOTT project and sees its logo...
- Outpox 10y agoThe pronunciation of "coke" is different from "cock". The pronunciation of "cock" is the same as the french word/animal "coq".
- lindbergh 10y agoActually, there's a slight difference between the two pronunciations, at least for the North American English pronunciation. When you say cock, there's an emphasis on the o (it lasts longer) while with coq, the o is slightly muttered. Like c-awk vs. c-uck, or according to wikitionary: \kɒk\ vs. \kɔk\ for coq.
- laurent123456 10y agoYes, and that's a strange choice of a name considering the whole website is in English (despite being from France).
- ritonlajoie 10y agowell, INRIA is french national research institute and the national pet is the Coq (rooster) (edit : laurent I guess you are french, I'm just saying that for those who are not from France :)
- minipci1321 10y agoIsn't it also somehow related to "Calculus Of Constructions"? Always made me think about that, not sure why.
- tomku 10y agoThierry Coquand is the creator of CoC and co-creator of Coq, so they're definitely related. :)
- progval 10y agoSome people say it's a revenge to “bit”.
- scrollaway 10y agoI've seen this remark quite often when the word (fr)"coq" comes up. It's a non-english word that's homophonous to (en)"cock", but... so what? In french, the word (fr)"bite" translates to "cock". It's pronounced like (en)"bit". And while a lot of people prefer "octet", "bit" has very much become part of the french vocabulary. So, what do we do? We don't care. We giggle at it when we're in high school and then it stops being funny. In Swedish, (en)"sex" and (en)"six" are the same word (se)"sex", pronounced the same way. They don't care. I also feel like some people here might be forgetting that (en)"cock" has other meanings in English, including the male bird which is what (fr)"coq" means Edit: Prefixed everything because this post was far too confusing.
- rhaps0dy 10y agoJust say "cock", with a straight face, not laughing and serious, and people will not laugh. People will know it's the proof assistant. Same when saying "Hoare logic".
- colanderman 10y agoAlthough I think the hairy ball theorem [1] is an exception to this logic. [1] https://en.wikipedia.org/wiki/Hairy_ball_theorem https://en.wikipedia.org/wiki/Hairy_ball_theorem
- deleted 10y ago[deleted]
- steego 10y agoIgnore the children. Coq is a fantastic tool! It's unfortunate people think of Coq as an academic language. I really think it's something more people should pull out at the workspace and not confine it to college experimentation. However the academic side of it is pretty slick. First, it's amazing how a few dozen lines of Coq can help explain the ins-and-outs of Hoare logic. (https://www.cis.upenn.edu/~bcpierce/sf/current/HoareAsLogic.html https://www.cis.upenn.edu/~bcpierce/sf/current/HoareAsLogic....). If you're into some really heady stuff and into homotopic types, the HoTT/Coq community has been explosive lately. While it's a great community, they can be a little particular when it comes to pull requests. Don't take it personally, Writing secure software will become a huge priority over the next few decades. There are many tools out there to create verifiable software, but I suspect there will always an opening for someone who can crank out rock solid Coq.
- deleted 10y ago[deleted]
- fusiongyro 10y agoI have one friend who gets squeamish about this, so I say it like "le coke" around him. Everyone else seems not to be bothered by it.
- ufo 10y agoThe list on https://coq.inria.fr/documentation https://coq.inria.fr/documentation is pretty comprehensive. Maybe Certified Programming with Dependent Types is along the lines of what you are looking for?
- jeffcoat 10y agoCertified Programming with Dependent Types http://adam.chlipala.net/cpdt/ http://adam.chlipala.net/cpdt/
- pron 10y agoHas anyone here ever used Coq to verify a non-trivial piece of production software? What was the experience like? (I have experience with other formal methods, a good amount of TLA+ and tiny a bit of Alloy and Why3, but I've never used Coq)
- progval 10y agoThere is CompCert, a C compiler
- pron 10y agoYes, I know about CompCert, but it took painstaking work by a world expert, and even he doesn't seem too thrilled about the process. So I'd love to hear a first-person account.
- maxiepoo 10y agoCompCert took painstaking work by many world experts, it was certainly not some heroic one-man effort by Xavier.
- nonsens3 10y agoSorry for the offtopic, but have you ever used TLA+ to verify a non-trivial piece of production software? I recently found out about it, and was wondering if there are good public use-case details on it! I know Amazon has used it for some of their production systems, such as S3, and DynamoDB, but couldn't find many details.
- martincmartin 10y agoThis is the one paper I know of: http://research.microsoft.com/en-us/um/people/lamport/tla/amazon.html http://research.microsoft.com/en-us/um/people/lamport/tla/am... I know of some small scale use at Facebook (where I work), where it has been used to verify a non-trivial protocol under various combinations of failures.
- tombert 10y agoI've been looking for an excuse to play with Coq (cough) for awhile now. A new release is as good an excuse as any I suppose. Does anyone know how this compares to something like Idris?
- nv-vn 10y agoIdris is meant for general purpose programming. If you want something Idris-like that is for theorem proving specifically, I would suggest trying Agda (which is much closer to Coq in terms of use).
- deleted 10y ago[deleted]
- chm 10y agoFWIW you would pronounce "Coq" much more like "kuhk" than "cock", if that makes sense. But that depends on the accent :)
- staticassertion 10y agoI think it's actually "coke", isn't it?
- jrmyp 10y agoIn French "coq" is \kɔk\, compared in to "cock" and "coke" which are \ˈkɑːk\ and \koʊk\ in English. It would be closer to "caught" \kɔːt\ with a short vowel and a \k\ sound at the end.
- pasquinelli 10y agomaybe i've got a weird accent, but "caught" with a "k" replacing the "t" is how i pronounce cock.
- jasonmp85 10y ago
- ohitsdom 10y agoThe first link in the post is a 404 for me: https://coq.inria.fr/coq-86 https://coq.inria.fr/coq-86
- mrcactu5 10y agoany reason to prefer Coq to Agda? And remind me what is the advantage over Haskell?
- ufo 10y agoCoq is more of a proof assistant than it is a general purpose programming language.
- wyager 10y agoCoq and Agda are both based on dependent types, but Agda is more of an in-progress research language whereas Coq is currently quite useful for doing proofs in practice. Haskell doesn't have full support for dependent types (yet). The Haskell community is very cautious with adding features that make type inference undecidable (like dependent types), so what people do is gradually add type system features onto GHC and then gate them behind feature flags. So you can do some of the things you can do in Agda in Haskell (like GADTs, kind promotion, limited type functions, etc.) but not everything. The advantage of Haskell's conservative approach is that it's actually very useful for writing programs, whereas Coq is only really meant for writing proofs and Agda is more of a research testbed than a production language.
- mitchty 10y agoEven when Haskell gets dependent types, they won't be quite as powerful as what agda/coq/idris have with the termination checks I believe. Which is fine, I don't think that many people want to program via proofs for everything. I'd say Idris is the closest to a useful general purpose programming language with proofs. At least that I've found so far, unless isabelle is? Not used it just came across it a while back and have to have a look. https://isabelle.in.tum.de/overview.html https://isabelle.in.tum.de/overview.html
- deleted 10y ago[deleted]
- Jweb_Guru 10y agoPeople actually use Coq to do useful things (this is kind of harsh to Agda but whatever). Haskell isn't really the same kind of thing (I mean, ostensibly you could write programs in Coq, and there are some extractors to other languages, but you generally use it as a proof assistant; by contrast, writing proofs in Haskell doesn't really work unless you happen to want to prove free theorems).
- primodemus 10y agoNice book that uses Coq: https://www.cis.upenn.edu/~bcpierce/sf/current/index.html https://www.cis.upenn.edu/~bcpierce/sf/current/index.html
- Girlang 10y agoWomen (not me!) will complain about the name and say "this is why there's no women in computer science."
- ah312 10y agoI guess this is as good a place as any, but has anyone used Microsoft's Lean before (http://leanprover.github.io/ http://leanprover.github.io/)? How does it compare to Coq? I'm really interested in getting started with formal verification, but I have a more "engineering" background and don't really know where to start. Coq, Isabelle, Lean... There's quite a few of these tools out there!
- pron 10y agoMost of the tools you mentioned are general theorem provers. They can be used for formal verification of software, but they are mostly research tools. Isabelle is probably the most production quality of those you mention. Industrial-grade formal verification tools -- designed for use by engineers and made to handle larger, more complex software -- include Z, TLA+, B-Method, Why3, SPIN, SCADE. My personal favorite is TLA+. You can start verifying real software in TLA+ in the same amount of time it would take you to get through the first one or two chapters in a book about Coq, and the size and complexity of systems you can affordably specify and verify are larger than you could ever hope to do in Coq. If you absolutely must have end-to-end verification, namely you must verify that global program correctness properties are preserved all the way to the machine code, then you should probably use SCADE if you're writing embedded real-time software; otherwise, consider Isabelle.
- sheepmullet 10y agoHave you used Z? How does it compare to TLA+? I'm thinking of trying out TLA+ this holidays to spec a couple of algorithms at work.
- pron 10y ago> Have you used Z? How does it compare to TLA+? I haven't used it but I've seen some examples of it. In many ways it is similar to TLA+, and Lamport says it's a nice, mathematical language. From an aesthetic point of view, it is less elegant: it has many more built-in concepts. From a pragmatic point of view, I think it does not support concurrency at all. Before creating TLA+, Lamport had intended to add TLA to Z for concurrency. This was the result: https://research.microsoft.com/en-us/um/people/lamport/pubs/pubs.html#tlz https://research.microsoft.com/en-us/um/people/lamport/pubs/... Anyway, here's a comparison by Lamport: https://research.microsoft.com/en-us/um/people/lamport/pubs/spec-book-chap.pdf https://research.microsoft.com/en-us/um/people/lamport/pubs/... > I'm thinking of trying out TLA+ this holidays to spec a couple of algorithms at work. Cool. Apart from being very useful, it's a lot of fun.
- LeanderK 10y agoI am currently hearing "formal Systems" at my university and that got me interested a bit. Can somebody comment why in practice it's so hard? In and ideal world I would image that certain languages are easier to prove (haskell vs C) and with the right tooling it should be able to prove many things quickly. Some things will always remain hard, but right now i don't see formal proofs of programs at all (i only hear some rumours that some companies use it at some small scale). So what's holding it back from being practical? Not enough engineer Man-power? Or is our theoretical understanding still not developed enough?
- tom_mellior 10y ago> In and ideal world I would image that certain languages are easier to prove (haskell vs C) It is. That's why Coq is a pure functional language, rather more like Haskell than like C. > and with the right tooling it should be able to prove many things quickly Yes, this should be possible, and it is possible. If you mean you want it to be automated: Isabelle/HOL has more automation than Coq. For many simple things, it suffices to tell Isabelle, essentially, to perform induction on a given variable and from that to try to find a proof automatically. It builds on several external provers to implement this. What is difficult is for the system to know which existing lemmas to reuse and how to combine them. It's a bit like your math homework, except that these systems know more lemmas (i.e., have a larger search space) and are not always good at ranking them by relevance. > right now i don't see formal proofs of programs at all (i only hear some rumours that some companies use it at some small scale) Look up SEL4 and CompCert for a start.
- LeanderK 10y agoOK, so if i want to build a program that proves my haskell code with a similar ease as using quickcheck[0] it would be possible, its just that nobody has done it yet and not that i would be nearly useless because i wouldn't be able to prove the most basic every-day functions. I would guess an database of previously proved lemmas for all the used libraries would help, so that you don't have to recompute everything. [0] quickcheck is an awesome library that generates unit-tests for specified properties (like: "for all lists s: length(sort(s)) = length(s)", i would then just generate a few hundred lists and check whether the property got violated)