4 ms·
Legend has it that Gérard Huet, who named Coq, enjoys double entendre and chose the name deliberately, just like he did with the Zipper data structure. So this
by tom_mellior 6y ago
Legend has it that Gérard Huet, who named Coq, enjoys double entendre and chose the name deliberately, just like he did with the Zipper data structure. So this might not be a great example of something that accidentally has a double meaning.
- bitwize 6y agoApparently some British researchers were working on a theorem prover named Bit, which in French sounds like "bitte" (slang for penis). So the French researchers who worked on Coq cheekily chose a French word with a double-entendre meaning in English. But all these anecdotes counteract what Wikipedia says, which is that Coq was named for one of its authors, Thierry Coquand, and for his "calculus of constructions" (CoC).
- ImprobableTruth 6y ago>But all these anecdotes counteract what Wikipedia says, which is that Coq was named for one of its authors, Thierry Coquand, and for his "calculus of constructions" (CoC). It being named after Coquand is unsourced and even states something that is outright wrong (Coquand is not Coq's "principal author", the best fit would be Huet and Christine Paulin, but even then it was developed by a team, they just lead it. Source: Coq's history page).