Hacker News Reader

Comment by iagooar | Hacker News Reader

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

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

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

Although I think the hairy ball theorem [1] is an exception to this logic.

[1] https://en.wikipedia.org/wiki/Hairy_ball_theorem

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

It's not homophonic with Coke?

EDIT: Inria is French (although Google translate insists the less fortunate homophone still exists in French).

The pronunciation of "coke" is different from "cock". The pronunciation of "cock" is the same as the french word/animal "coq".

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.

That's how I pronounce it haha. Or I say "the INRIA prover."

Wait till the GGP hears about the CoqHOTT project and sees its logo...

Yes, and that's a strange choice of a name considering the whole website is in English (despite being from France).

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.

'Bit' does not translate as 'octet'. 'Byte' does.

Minor remarque changing nothing in the meaning of your message.

And actually byte and octet aren't identical (octet is less technically ambiguous, since bytes aren't always 8 bits but octets are.)

That's a really cool point I never realized!

Uh, you're totally right. I'm completely losing my french, not using it :)

PS: remark, not remarque ;)

> 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

Which (en)"cock" does (fr)"bite" translate to?

The genitalia.

Wouldn't "bite" in French sound more like "beet" in English?

Yes, but in french, (en)"bit" is also pronounced with a longer "i" sound than in English, so "bit" in french is also pronounced more like the english "beet".

Try playing with https://translate.google.com - the audio is very fair on it (albeit spoken much slower than you normally would).

Some people say it's a revenge to “bit”.

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

Isn't it also somehow related to "Calculus Of Constructions"? Always made me think about that, not sure why.

Thierry Coquand is the creator of CoC and co-creator of Coq, so they're definitely related. :)

It's almost certainly a bit of a joke on anglophones. I mean, just look at their logo.

not a joke, but a wellspring of bad jokes.

The name was picked by French people who were not aware of the English word.

Sure, and French don't have a word for "entrepreneur" neither

They were certainly aware of the english word. But I think they are too proud of their mother language to care :)

oh they care, that's why they went with the name IIRC. native english speakers being uncomfortable with the name was an advantage.

The list on https://coq.inria.fr/documentation is pretty comprehensive.

Maybe Certified Programming with Dependent Types is along the lines of what you are looking for?

Certified Programming with Dependent Types

http://adam.chlipala.net/cpdt/

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.

Reply on news.ycombinator.com