6 ms·

Is there a good book about more advanced usage of coq?

by iagooar 10y ago

Others 10y ago
That's not surprising, since that's the correct way to pronounce it...
- hawkice 10y ago
  It's not homophonic with Coke? EDIT: Inria is French (although Google translate insists the less fortunate homophone still exists in French).
  - nickpsecurity 10y ago
    That's how I pronounce it haha. Or I say "the INRIA prover."
  - theoh 10y ago
    Wait till the GGP hears about the CoqHOTT project and sees its logo...
  - Outpox 10y ago
    The pronunciation of "coke" is different from "cock". The pronunciation of "cock" is the same as the french word/animal "coq".
    - lindbergh 10y ago
      Actually, 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 ago
  Yes, and that's a strange choice of a name considering the whole website is in English (despite being from France).
  - ritonlajoie 10y ago
    well, 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 ago
      Isn't it also somehow related to "Calculus Of Constructions"? Always made me think about that, not sure why.
      - tomku 10y ago
        Thierry Coquand is the creator of CoC and co-creator of Coq, so they're definitely related. :)
  - progval 10y ago
    Some people say it's a revenge to “bit”.
  - scrollaway 10y ago
    I'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 ago
Just 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 ago
  Although 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 ago
  Ignore 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 ago
I 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 ago
The 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 ago
Certified Programming with Dependent Types http://adam.chlipala.net/cpdt/ http://adam.chlipala.net/cpdt/

Is there a good book about more advanced usage of coq?

by iagooar 10y ago

Is there a good book about more advanced usage of coq?

Others 10y ago

That's not surprising, since that's the correct way to pronounce it...

hawkice 10y ago
It's not homophonic with Coke? EDIT: Inria is French (although Google translate insists the less fortunate homophone still exists in French).
- nickpsecurity 10y ago
  That's how I pronounce it haha. Or I say "the INRIA prover."
- theoh 10y ago
  Wait till the GGP hears about the CoqHOTT project and sees its logo...
- Outpox 10y ago
  The pronunciation of "coke" is different from "cock". The pronunciation of "cock" is the same as the french word/animal "coq".
  - lindbergh 10y ago
    Actually, 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 ago
Yes, and that's a strange choice of a name considering the whole website is in English (despite being from France).
- ritonlajoie 10y ago
  well, 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 ago
    Isn't it also somehow related to "Calculus Of Constructions"? Always made me think about that, not sure why.
    - tomku 10y ago
      Thierry Coquand is the creator of CoC and co-creator of Coq, so they're definitely related. :)
- progval 10y ago
  Some people say it's a revenge to “bit”.
- scrollaway 10y ago
  I'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 ago

Just 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 ago
Although 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 ago
Ignore 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 ago

I 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 ago

The 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 ago

Certified Programming with Dependent Types http://adam.chlipala.net/cpdt/ http://adam.chlipala.net/cpdt/