Instrumentul de demonstrare a teoremei Coq se gândește să-și schimbe numele. Motiv: Pentru anglofoni, cuvintele „coq” și „cocos” (argo pentru organul sexual masculin) sună asemănător, iar unele utilizatori de sex feminin au întâlnit glume cu dublu sens când folosesc numele în limba vorbită. Însuși numele limbajului Coq provine de la numele unuia dintre dezvoltatori, Thierry Coquand. Asemănarea sunetului Coq și Cock (cocoșul englez) a fost deja redată în proiect: limbajul folosit pentru a descrie structurile se numește Gallina (pui latin).
Sursa: opennet.ru