News for hackers. Stuff that matters.

A comment on Coq: Certified Programming with Dependent Types.

Re:Coq: Certified Programming with Dependent Types by bencollier49 on Friday July 10, 2015 @06:20AM (#9863127)
I assume that this wasn't originally created by an English-speaking dev team? Or at least a very serious and formal one?
[ Parent | on HN ]
Re:Coq: Certified Programming with Dependent Types by groar on Friday July 10, 2015 @08:04AM (#9863403)
There are many reasons for the name: apart from being one of France's emblems, one of the people who initiated the project is Thierry Coquand and the original type system underlying it is called Calculus Of Construction (CoC).

But I know for a fact that they thought it would be good joke as well.

  Or at least a very [...] formal one
That's a good one ;)
[ Parent | on HN ]
Re:Coq: Certified Programming with Dependent Types by liotier on Friday July 10, 2015 @06:26AM (#9863140)
It originated in France (see https://coq.inria.fr/about-coq). In French, 'coq' means 'rooster' - the language that implements Coq is named Gallina and the logo is indeed a rooster.

Well, no worse an homophone than 'bit' to French speakers...

[ Parent | on HN ]
Re:Coq: Certified Programming with Dependent Types by throwaway999666 on Friday July 10, 2015 @06:58AM (#9863207)
The language and ideas behind it seems pretty serious. But they might consider pissing off particularly prudish Americans to be a bonus.
[ Parent | on HN ]
Re:Coq: Certified Programming with Dependent Types by justinpombrio on Friday July 10, 2015 @09:22AM (#9863756)
A few timid speakers will mispronounce it like "coke", but everyone knows they're saying it wrong.
[ Parent | on HN ]
Re:Coq: Certified Programming with Dependent Types by eli_gottlieb on Friday July 10, 2015 @10:01AM (#9863975)
It's pronounced identically to "caulk", though, not "cock".
[ Parent | on HN ]
Re:Coq: Certified Programming with Dependent Types by Afton on Friday July 10, 2015 @12:30PM (#9864954)
In my idiolect, those two words are homonyms. When I worked construction, you couldn't ask someone for caulk without raucous laughter.

http://dictionary.reference.com/browse/caulk

this link seems to agree, with the word represented in IPA as [kɔːk]

[ Parent | on HN ]
Re:Coq: Certified Programming with Dependent Types by davidgrenier on Friday July 10, 2015 @12:21PM (#9864874)
Not 100% confident on how people pronounce "cock" but it's definitely not close to "caulk".

Being a french speaker, I would say pronunciation is closer to "puck" with a k, so go with "Kuck".

[ Parent | on HN ]
Re:Coq: Certified Programming with Dependent Types by davidgay on Friday July 10, 2015 @10:18AM (#9864060)
More like somewhere in between, really.
[ Parent | on HN ]
Re:Coq: Certified Programming with Dependent Types by innguest on Friday July 10, 2015 @02:09PM (#9865663)
More information about who in the US has and hasn't merged those two sounds: https://en.wikipedia.org/wiki/Phonological_history_of_Englis...

It's the cot-caught merger.

[ Parent | on HN ]
Re:Coq: Certified Programming with Dependent Types by cjensen on Friday July 10, 2015 @12:43PM (#9865055)
Intentionally pissing off people is childish.

Using the name of this language in a workplace creates a hostile working environment[1]. That guarantees that no sensible person in the English speaking world will ever use the language at work.

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

[ Parent | on HN ]
Re:Coq: Certified Programming with Dependent Types by throwaway999666 on Friday July 10, 2015 @03:00PM (#9866037)
> Using the name of this language in a workplace creates a hostile working environment[1].

Oh my, thanks for the laugh. I half imagined a Dilbert scenario when reading that.

It's weird to think of the simultaneous uptightness and childishness which would make it impossible to use this homonym in the proper context.

[ Parent | on HN ]