The name Coq comes from the French word for rooster, CoC (the Calculus of Constructions) and Thierry Coquand, one of the initial authors of Coq. But it is also close to the word "cock" which has a slang meaning that some English speakers consider offensive (it also means a male bird or the firing lever in a gun). This similarity has already led to some women turning away from Coq and others getting harassed when they said they were working on Coq. It also makes some English conversations about Coq with lay persons simply more difficult.

This page is about collecting ideas for alternative names or alternative pronunciation strategies. When new ideas stop being proposed, we can start a survey of the Coq community to see what its members would think of the proposed alternatives. The existence of this page is not yet a commitment toward a renaming. This will all depend on the community feedback (especially with the survey).

Anyone is welcome to add to this page (new ideas, but also arguments in favor or against one idea in particular). Do not delete content added by others please.

These alternative pronunciations could be recommended to English speakers in particular, or made official.

Advantages: Simple, not everyone has to do it. Disadvantage: Not everyone will do it. The sound in French is not great. Hint: in French it is better to avoid spelling out the letter 'Q'.

(Tadeusz Litak) If the French sound is not great and would lead to Q being dropped, it’s not a good proposal. A solution which would not go down well in France is a non-starter. As for “Not everyone will do it” though: let us not fool ourselves that any change will be fully universally adopted; not with a legacy stretching back four decades.

(kf) Maybe have a relevant backronym to go alongside it?

I don't see that any alternative pronunciation strategy can work well. The point of the change is to ease communication with those outside the community, whose default (English) pronunciation would still be "cock", and one also doesn't want to have to explain a non-standard pronunciation whenever introducing it. Spelling COQ is the least bad of these options, but rather clunky.

Advantages:

• From one anglophonic perspective, it's reasonably natural, close-ish to the original, and non-offensive (of course, I [Joshua Grosso] assume there would be significant detriments for e.g. francophones, so please take these with a grain of salt). At least one anglophone I [Joshua Grosso] know uses this pronunciation already to avoid offensiveness.

Disadvantages:

• Some anglophones also speak French; this suggestion may feel quite awkward to them (it does to me [Benjamin Pierce]). IMO this is strictly dominated by the see-oh-queue suggestion.
• I [Yannick Zakowski] agree with Benjamin, and would add that all options that rely on subtly pronouncing the same "word" differently (i.e. like "gok" or "coke" rather than "cock") are probably too subtle for non-native english speaker. I at least sincerely have a hard time pronouncing with confidence the differences between the proposed "gok", the French "coq" and the American "cock".
• (Tadeusz) further down on this list there is a proposal to add the circumflex to the French spelling, which would apparently help to match the pronunciation. In combination with adding the French definite article to the official name, it might be an interesting combo. “Le Côq (Formel)”: that doped theorem-proving rooster of ours. Or perhaps “LeCôq”, as spelling the name as a single word is apparently preferred by quite a few people. And the fact that this pronunciation has already been adopted and even promoted by some people should be also taken into account.
• Subtly different pronunciations also run the risk of simply not being used and of making it harder to search for coq on the internet. It might be preferable to use a name that is distinct enough that the search engine of your choice will correct it if misspelled.

Advantages:

• Mostly the same as coke, feels more natural to me (Robert Rand).
• Doesn't sound like a drug or like it was sponsored by a soda company.
• Cook is a relatively common name; born by at least one famous computer scientist (of Cook-Levin theorem fame).

Disadvantages:

• Far from being evident from the spelling.

Probably cute in English but in French, it sounds close to "cocu" which is a deceived husband.

Himada4: Little fun fact: "Kokyu" in japanese means to breathe

Note: the French pronunciation has no "G" sound. But if it works for native English speakers, fine.

Disadvantages:

• Seems awkward in both French and English (Benjamin Pierce).
• French has a "G" sound?

Given that the misunderstanding often relates with the lack of context, maybe adding the context in "Coq theorem prover" will make sure the listener has the right context (even if they have no idea of what a theorem is, they understand is some complex math concept). This has the advantage of not requiring any change, just some awareness of the speaker.

If that is not considered enough by Anglophones, you can use the full French version (Le Proveur Coq or le prouveur de théorèmes Coq or L'Assistant de Preuve Coq) making it sure that you are using words from another language. (Francophones, please change this proposal so it matches the most common name in French). This works the same way as the brand le coq sportif.

Advantages: no name change, honors the French heritage and promotes more diversity.

Disadvantages: would probably still be shortened to "Coq" in conversation, and a lot of anglophones will probably butcher the French pronuncation (in the case of "Le Proveur Coq", although maybe this isn't an issue in-and-of-itself).

Hugo: note that the exact French word for "prover" is "prouveur"

Endgame: I don't really work with Coq, so my opinion isn't worth much. But I like that Le Prouveur Coq respects the French heritage. As an Anglophone who butchers every language, I'd probably just call it "LPC" ("ell pee see").

Variant of the above, with possible French alternative: Coq, le Prouveur Interactif de Théorèmes. New papers referring to Coq would write "the Coq PIT".

See also below Coqpit as a new name.

Another variant, with English pronounciation "kok'ai-ti-pi".

Follow-up of the proposal above, but without an explicit English translation so English people also say it the same way I guess it works for "Le coq sportif", and the word "formel" is very similar in many (at least European) languages.

We can also benefit from the logo change and a careful choice of the font for the name to give Coq a fresh look without changing the original spirit of the name.

Advantages: no change for the command names, honors the French heritage and promotes more diversity.

(Luc Pellissier) It would have LCF as an acronym, which might be a clever pun, but also a bit confusing.

=> An acronym should not contain articles so the acronym would really just be CF.

Solves the issue, and underlines the French origin of the software. Plus, reminds of Le Lisp: https://en.wikipedia.org/wiki/Le_Lisp , a former French Lisp implementation from INRIA, too.

Has the double meaning of a cook and a rooster (in addition of the scientific origin: CoC and Coquand). Liable to please also the amateurs of Estonian beer. Possible variants: LeCoq or Lecoq.

(Tadeusz): The “LeCoq” variant seems preferred. Also, as pointed out by Paolo Torrini: “LeCoq (especially if pronounced 'lecoke') could actually even sound like a nice, if belated, acknowledgment of an early connection with the LEGO system”

(Grosso): It feels a bit weird to me as an anglophone to have "The" be part of the name proper (the first thing that comes to mind is "The Batman"). But not the end of the world either way, especially given that English is not the only audience here :-)

Disadvantages: This runs the risk of worsening the problem instead of improving it since "Le" has been used in 4chan a lot (info). To people familiar with meme culture "Le Coq" could be understood as an invocation of the rage comics context which – as it is juvenile and masculine – could strengthen the anatomical association instead of weakening it.

(Tadeusz): An interesting point, but I think it overestimates the familiarity with 4chan meme culture among both academics and the general public. If one takes such objections seriously, I think that “... Formerly Known As Coq” issue is a bigger concern. Several people claimed that the goal shouldn’t be something that can’t be misinterpreted or abused at all, but just something that doesn’t invite puns on more or less every occasion. Plus, it seems it does not affect so much the “LeCoq” spelling: from what I’m seeing, 4Chan uses “Le” as a proper article. BTW, I took the liberty of merging the two different occurrences of “Le Coq” on this list.

Other disadvantage: Adding "Le" in front of something is a very non-French way of making something sound French, why not add "baguette" to be even more cliché?

To avoid losing the word Coq, which is already used in many academic papers but also in the names of many tools and libraries.

The package and command-line tools wouldn't change name.

The package and command-line tools would change name (gallinac, gallinatop, etc.).

(Arthur Azevedo de Amorim) The Portuguese cognate "galinha" can be offensive. (Rémi Nollet) For those who do not speak Portuguese: what would it mean? (Arthur) It means "promiscuous person", usually a woman.

Note: gallinac is a cute pun in French ("Gallinacées" is a common name for the order of Galliformes); gallinatop also sounds rather nice.

Related to the above suggestion of switching to Gallina: the trailing "o" reflects that there is no formal definition of what Coq (the Proof Assistant as a whole, distinct from Gallina, Ltac, and the rest, which already have fine names) is, apart from its OCaml implementation.

In English, it will probably be heard as "cocoa" as in "hot cocoa", a delicious winter beverage, or perhaps bring to mind Coco Chanel, the famous French fashion designer.

Coco is a French name (or nickname, I'm [Cyrus Omar] not sure), so French speakers will find it familiar I suppose? Though reading below on "Koko", it sounds like it may be slang for "communist" in France as well? Would a French speaker assume it refers to communism rather than the nickname "Coco"?

One possibility is to pronounce it as "Coco" when speaking English and "Coq-o" in French.

Coqo as spelled still embeds "Coq" so it will probably be clear when someone reads a prior paper mentioning Coq that it is connected to what is now known as Coqo.

I'm (Matthieu Sozeau) not sure it is a good idea to confuse the Coq assistant with the existing Gallina language. How about we use Gallo for the assistant instead? There is an obvious confusion with the (somewhat declining eastearn britanny language)

https://en.wikipedia.org/wiki/Gallo_language

(Xavier Leroy) Gallo is a (natural) language, so it's closer to Gallina (a language) than to Coq (a tool). Plus, as you wrote, it's "somewhat dying" as a language, which does not bode well.

(Matthieu Sozeau) Agreed, not such a good idea.

(Alberto Fiori) Gallo is also the italian word for rooster, it would be a nice dual Gallina (the italian word for chicken)

(Robert Rand) I don't think enough people are familiar with the Gallo language for this to be a concern.

Short for "Rocquencourt", the place Coq was started at (from the manual: "Coq is the result of more than 30 years of research. It started in 1984 from an implementation of the Calculus of Constructions at INRIA-Rocquencourt by Thierry Coquand and Gérard Huet.")

• Short name, doesn't seem to be in use
• Close connection to the history of the system
• Keeps the letters c, o, q
• Closest English and French words are "rock" and "roc" (hard stones), with no bad connotations.
• In fact, multiple good connotations (bedrock) and opportunity for wordplay (Coq hacker => Rocq star)

(See below for note that Roc / Rok / Rokh is also a mythical bird)

Talia: I like this too; it's meaningful and a really easy switch to make verbally.

(Tadeusz) Apart from the fact that it would often get referred to as “Rocq/Coq”, it paves the way for other puns such as “Rocq-hard proofs”. But it’s up to native speakers to decide if they see a problem in this.

This sounds good in spoken English. "Rock" generally has good connotations of solidity and strength, the Rocquencourt connection is nice, the "Rocq" spelling is rare on Google, and there's no problem with "Rocq-hard" that I can see.

Regarding the spelling, some native speakers reported in the Zulip chat that they’d find it confusing to pronounce.

In case one tried to read it as an acronym, here's a try: Real-world maths, Objective-camel implemented, CQ based proof assistant (where CQ would stand for the appropriate extension of Coquand/Huet's CoC).

Downside: The name Rocq could be confused with the ML-family functional programming language Roc (named after the mythical bird) - https://roc-lang.org

Coq would be viewed as an abbreviation. This has precedent, for example in programming languages that are named after persons, such as Haskell, Pascal, Ada, etc.

An advantage would be that it would avoid renaming related projects and command-line tools. Packages should probably be renamed though.

Talia: I really like this. The only slightly weird thing about it is that he is alive, which makes it maybe a bit awkward. But maybe not; I think naming theorems and algorithms after people often happens while they are still alive.

The creator's first name which, in English, can be pronounced as the word "theory" which would feel appropriate. First names have been used by other programming languages, such as "Haskell."

If we really wanted we could try to make it an acronym (backronym). Open to suggestions there.

Pioneer and visionary. Possibly the guy responsible for the mess.

(Alain : Oui, on programme en Haskell et on prouve en Gérard !)

Maybe this could also be written CoQed? Anyway, it could be understood as Co=constructively Qed=proved, a nice in-joke.

The 'coked' pronunciation is a minor variation on the 'coke' theme already used by someone. The alternative 'co-q-e-d' one seems also nice. There's hardly any drug reference (someone who's on cocaine is 'coked up', not just 'coked'). In fact, 'coked' coal is an important ingredient in steel production.

Can alternatively be pronounced with two distinctive syllables: "Ko Ked"

A translation of the French word. Watch out: "rooster" is also slang for "penis", e.g. https://www.urbandictionary.com/define.php?term=rooster

(Jasper Hugunin) While "rooster" and "cock" are both slang for "penis", there is a large difference in frequency of use, primacy of other definitions. Used in isolation, or heard as a snippet of conversation, "cock" almost always means the male genitalia, while "rooster" first brings to mind the bird, and requires large contextual clues to change meaning. (Background: 23 year old male American, first language English, attended US public high school not too long ago.) But yes, it is possible to turn "rooster" into a vulgar joke as well, it's just much harder, while the jokes write themselves for "Coq".

(Tadeusz) Is “Rooster (Formerly Known As Coq)” really such a great idea? But Paolo Torrini’s suggestion to use “Roost” sounds better.

(Arthur AA) I don't get this point. "X (Formerly Known as Coq)" sounds bad for any value of X.

(Tadeusz) Exactly. That is the point. Everybody arguing for a departure from Coq’s present name should keep it in mind. Still, for some values of X it’s worse than for others.

(Dan Frumin) It worked for Prince, at least. The Proof Assistant Formerly Known as Coq (TPAFKAC).

(Tadeusz) Yes, and this proposal is actually discussed below. I rather like it. Unlike the “X (Formerly Known As Coq)” approach, it tackles the problem head-on.

(Rebane) I'm not a native English speaker, but to me “Roost” sounds too close to the Rust programming language to cause occasional mix-ups.

"Chook" is Australian slang for a chicken, and might be close enough to Coq by being a similar animal.

This is the latin word for "rooster" and the genus for assorted fowls including gallus gallus domesticus, the familiar chicken/hen/rooster. It also means "Gaul", as in nos ancêtres les Gaulois, making a connection with France. There's also a connection with gallium, the chemical element number 31, and its discoverer, Mr. Lecoq de Boisbaudran, but it is far fetched.

Gallus is also a Scottish adjective meaning bold, cheeky, or flashy.

[Meta-suggestion: any proposal should be checked online and in dictionaries of relevant languages]

(Jasper Hugunin) A bit of a stretch, maybe not disqualifying, but as a native English speaker (and given the context of this page), Gallus reads a lot like "phallus" to me, which is again a name for male genitalia.

(Tadeusz): Just as above. “Gallus (Formerly Known as Coq)” hardly sounds like a PR triumph.

(Rémi Nollet) “Gaul” is not Gallus but Gallia. That is the pun. Something else: Gallium is also the former name of the Inria team developing OCaml, which is also a nice link.

(Rémi Nollet) See the discussion on the previous proposition (Gallus). With Gallia, we gain the fact that it does not sound like phallus, and we lose the fact that it is an actual translation of Coq. We keep the reference to Coq and to France as well as the proximity with Gallina.

Sounds like "goal", keeps French connotation?

Disadvantage: "Gaule" can be definitely used to mean "erection" in French.

(Tadeusz) Proposed on the mailing list by Paolo Torrini for the Gallina-Coq combo. I have to say that of all Gallina-based name variants, I find this one most attractive. OTOH, it does rhyme with “phallic” and “Galliq (Formerly Known as Coq)” sounds unconvincing.

A short portmanteau of Gallina + Coq.

Another short portmanteau of Gallina + Coq.

+: A minimal diff from Coq.
+: Apparently corresponds to the french pronounciation of Coq

Something entirely different - more looking into the future than the past.

Not so good when combined with Coq!

It's both a name and a word, and it's the same word in both English and French. It means dead certain, a certainty. It has positive (Positivist?) connotations. It communicates the essential purpose of the proof languages and system. Its use is established, as in "CompCert." It's not taken as the name of a language, AFAICT. It sounds good.

Worth considering the French spelling "Certes"? (the anglophone reading may be a little confused, but even with a pronounced "s" it's quite charming)

To keep a French name. A less offensive chicken.

https://en.wikipedia.org/wiki/Capon

Keeping both a French name and some reference to chickens seems attractive from both historical and political points of view. (Benjamin P.)

This is probably the most honest new name since a Chapon used to be a Coq, and we might consider the avoidance of the sex joke as akin to an emasculation, so it both fixes the problem and stands witness to what happened.

I think this chicken is less offensive because it's missing something. (T. Bourke)

(Jasper Hugunin) Not a French speaker, don't know how common the knowledge of what makes a Chapon is, but as an English speaker Chapon sounds like a nice name.

This actually involves reference to something that, in someone's book, might count as cruelty to animals (capons are castrated to get them forcibly fat).

(Matthieu Sozeau) I wouldn't want the software to be identified with mutilated X

Used to be the calculus before it became the unpronouncible PCUIC. Can be pronounced "see-I-see" or "kick". Positive connotations:

• "Kick it!"
• "I get a kick out of doing CIC proofs!"

Like GNU, this can be viewed as a recursive acronym: CIC is Coq

(mmalter) It's the name of a bank in France...

small shift, still a joke.

Talia: My advisor (Dan Grossman) notes this can be pronounced "cookie" in English which is really cute.

And it has "coq" as a prefix. This one might be pretty good. (Benjamin Pierce)

This is not a great name for a Russian speaker: it sounds like "коки" which has a slang meaning "testicles". (Anton Trunov)

small shift, still a joke.

the Calculus Of Inductive Qonstructions

(Théo Zimmermann) If we adopt this one, we should make sure people pronounce it \kwa.k\

Natural English pronunciation like "clock". Advantages: looks and sounds pretty similar to coq, at least in English; not too many Google clashes; one-letter change; phrases like "I'm working on cloq proofs" sound ok.

Disadvantages: similar to the French word "cloque" which means blister and blight, and is also used in slang expressions about pregnancy. E.g., "Je viens de mettre ma preuve en cloq".

A clam, so the English could just be a different animal. French could still be Coq, no need to rename packages. Kind of sounds like "Coq" blended with "Gallina." Could probably also backfit with features: "u" for universes, "i" for induction, anything else new since Coq was mostly just CoC?

Derek notes, from Wikipedia: "Coquina (/koʊˈkiːnə/) is a sedimentary rock that is composed either wholly or almost entirely of the transported, abraded, and mechanically sorted fragments of the shells of mollusks, trilobites, brachiopods, or other invertebrates." Which has lots of type theory joke potential.

Hugo: In French, Coquina is liable to be perceived as a cognate of coquine which can be used affectionately but not always. (Guillaume: I have not though about this link)

Derek: Given the apparent sexual connotation of "coquine", it would be best to avoid Coquina (sadly).

A scallop-based dish in English; scallop in French. In English people pronounce the "l." Also probably possible to stuff into an acronym, and same upsides as Coquina. If the French don't really enjoy being represented by a scallop, still possible to call it Coq in French.

Hugo: In French, coquille is more generally shell (of egg, snail, seashell, ...), not only scallop kept with its shell.

JH. It is also a "typo", with a specific story of the letter q disappearing. We could probably avoid this one ...

The fruit of the native palm tree of Chile. Sounds cute in English. French could still be Coq, no need to rename packages. Could probably also backfit with features: "u" for universes, "i" for induction, what else?

Yannick Forster: Coquito is also the name of a Puerto Rican eggnog. And apparently in Colombia, Puero Rico, and Venzuela colloquial for "blow to the head with bare knuckles" (if I understand the seventh meaning here correctly: https://es.wiktionary.org/wiki/coquito).

Félix Fischer: Yannick, you're right. Although it is not exactly a blow to the head as in say, boxing. (CW: violence) It is a coscorrón, which is more like... a soft (though still painful) knuckle-hit or knuckle-rubbing at the top or sides of the head. It's part of what's hopefully a dying tradition of mothers (though sometimes other elder relatives) using physical pain to teach stuff to their children. The intent is usually of love, but definitely misguided. (Look up "don ramón coscorrón" in YT and you'll see an example of one. It might be slightly exaggerated, so take it with a grain of salt)

Calcul Universel Inductif (Universal Inductive Calculus)

Sounds like a baby chick's cry.

Cuy is the the name for Guinea pigs in parts of Latin America, keeping up with naming things after animals.

Offensive in French.

Calculus Handling Inductives Completely Kernel Errors Notwithstanding (the second C may also be read "Competently", "Consistently", etc)

(Tadeusz) The acronym is awesome. I would just replace the first word with “chicken”, making it a recursive one... or with “Coq”.

(Arthur AA) There is already a Scheme compiler called Chicken (https://www.call-cc.org/).

A pretty bird that never upset anyone. And "p" for proof.

Logo could be reused / adapted as it stays in the "Gallinaformes" area according to wikipedia. Sound is still close to the original one which would help transitioning.

Pcoq is already the name of a graphical interface to Coq, developped by the Lemme team at Inria Sophia (but no more maintained) https://www-sop.inria.fr/lemme/pcoq/

French for "peacock", similar reasoning to pCoq/PeaCoq

Keeps the French animal tradition, uses a bird

short

can't find any existing languages using it

How do you pronounce it in English?

• sort of like "paun" or "pawn"
• IPA: [pɑ̃]
• google pronunciation: https://www.google.com/search?q=comment+prononcer+paon

It can sound a little bit like "porn".

"Proof Assistant" could be the start an English backronym

A fitting name for a tool used to assist theorem proving. Preserves a joke for people that really want to make one. Acknowledges that at some point the name was close in pronunciation, whereas the second one is close in writing. Also is a reference to cockfights, even if it is an unethical practise.

(Tadeusz) I really like the Coqpit idea (with this spelling). Some sets of slides introducing UPenn’s lecture on Software Foundations are illustrating progress that one makes when studying Coq starting from a joystick, through a game console, up to a full-blown plane cockpit after years of study. The only confusion that I see is:

https://github.com/LumaKernel/coqpit.vim

Because Côq is an extremely addictive tool. In French, it would be pronounced with a closed "o" reminiscent of the "o" of "coke" in English. Good for those fond of playing with words, oh geez, these lines of high quality Côq made me so happy.

(Tadeusz) Shouldn’t it be merged with the “coke” proposal above? Actually, changing the officially approved pronunciation and the spelling (and possibly adding “Le” in front to top it off) sounds like a powerful combo.

"Coq au vin" is already a phrase using the French word "coq" that many Anglophones use and will highlight that it is not the English word "cock." I don't know if there are any opportunities for culinary references involving Coq, but using other French words in the phrase will highlight (in English conversation) that it is a French word.

Disadvantage: The name "Coq au vim" has already been coined, for a vim extension.

A portmanteau of "Proof" and "Roost", and also an homage to the great French writer Marcel Proust. Also, Proust's famous "madeleine" cookie has the shape of a shell (or "coquille").

( n.b. possible unnecessary confusion with a Scala library also called Proust for software transactional memory - https://github.com/ScalaProust/ScalaProust/ / )

( Also possible confusion with ASAP compile-time memory management, which is sometimes called Proust for short. - https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-908.pdf - https://github.com/doctorn/micro-mitten#how-can-i-use-it )

Calculus Of CORrect Inductive COnstructions

I should clarify for non-native French speakers that this is the onomatopoeia corresponding to the rooster's crow in French. So equivalent to Cock-a-doodle-do in English or Kikeriki in German.

Possible confusion: The Coq Wiki used to be called Cocorico (the license footer on this page still mentions the name).

No acronym, just a reference to the rooster's crow in French as COCORICO above. Might not need renaming of the tools, because the toolname coq can still be short for Coqorico. Might also be less confused with the former Coq wiki.

A faux-French spelling of "chocolat", meaning "chocolate" in English. It's got an embedded "Coq", honoring its heritage, and who doesn't like chocolate?

If kids can sing it (and Old MacDonald), you can say it!

Using ACL2 convention, the name "C2" or "CC" can be considered as abbreviation of "Calculus of Constructions", the logic behind Coq.

(kf) There's a programming language with that name.

Using ACL2 convention, the name "C2" or "CC" can be considered as abbreviation of "Calculus of Constructions", the logic behind Coq.

(el) There's no programming language with this name.

(kf) But traditionally Unix systems have cc symlinked to the C compiler. If the binary name changes as well this will be a problem.

(unk) But wouldn't the binary name be ccc, short for 'CC Compiler'?

(el) As Unix is case-sensitive, it's difficult to confuse a C compiler cc w/ a proof assistant CC.

Acronym for "Coq Proof Assistant."

Advantages: retains the original name (which may be important for the French research community), but the spelling and English pronunciation are further removed from the current name than "see oh cue" or "coke."

Disadvantage: unfortunate associations with Barry Manilow and https://en.wikipedia.org/wiki/Raymond_Kopa

(Tadeusz) Don’t know if there is something problematic about Barry Manilow, but who has issues with Raymond Kopa? Coq can even officially adopt “Kopaszewski” as its full name.

French for "whooping cough", with a secondary meaning of a highly fashionable trend.

Advantage: retains the original name, quite positive association in French

Disadvantage: maybe hard to pronounce for English speakers?

(Tadeusz) Is a potentially deadly disease against which people are vaccinated really such a good brand?

Advantage: The meaning is quite obvious, it is not a French word, but the french translation is only one letter away (and could be taken alternatively). It connotes of professionalism and assistance in doing something elaborate.

Disadvantage: The "co" root is preserved, but not the association with French symbols.

Exploring other chicks.

Anothe translation of chicken

A strong monster from the nethack games.

https://nethackwiki.com/wiki/Cockatrice

+: Sounds pretty powerful.
+: Its relationship to Coq is nicely explained in the definition (above).
+: Also connotes an animal, like Coq, OCaml, etc.

-: People may prefer to abbreviate it to Coq.
-: (Matthieu) WOW that's intense!

+: (Tadeusz) I see the two minuses above as pluses. I am firmly of the opinion that it should be something that still can be abbreviated to Coq. And there is nothing wrong with the name being intense. The only question is French spelling. The French wikipedia gives the following options: cocatrix, coquatrix, caucatrix or cocatrice. “Coquatrix” is nice: not only it abbreviates to Coq, but it shares most of its part with Coquand (see below for my next proposal based on a variant of this one). The only possible confusion I see:

https://en.wikipedia.org/wiki/Bruno_Coquatrix

A variant of the above proposal. The monster begot by Coquand and hatched from Coq’s egg. The glance of its eye sufficeth to turn to a rocq-solid proof any living thing that standeth before it. An attempt to look at itself in the mirror (prove its own consistency) would immediately kill it though.

https://fr.wikipedia.org/wiki/Cocatrix
https://en.wikipedia.org/wiki/Cockatrice

Tadeusz' original French version

The shortest version of all

Another possibility is take advantage of a current hole in the system name scheme: the tool/project is named Coq, and the functional programming language is named Gallina, but we have no name for the Coq document format as such [which is extensible]. Thus, we could use a name "Whale" and people could say "I am writing Whale proofs".

Some names that were discussed for such a document format a couple years ago were:

• PLoF "Protocol for Logical Formalizations"
• YASPD "Yet Another Standard for Proof Documents"

But IMHO there are not really suitable.

Another idea:

• FLGC The "Fowl Language for Grivois Connections"

In English, toque rhymes with "coke". On the other hand "toque" is not a widely used word, at least in North America, as far as I know. I believe the Canadian "tuque" originates from that, but it might be obscure enough that we would still have to tell people that it is pronounced "coke" in English. Also, I don't know if there are any negative connotations in French.

Coque and coq have the same pronunciation in French, the only difference is the gender of the noun. Also consider the standard clam (coque) metaphor for female genitalia.

OK, this one can be deleted. We are back to the same problem.

Cocon is the French word for Cocoon. This keeps both the animal theme and the CoC joke. Could be rewritten and stylized as CoQon if we want a hybrid animal theme, and keep the rooster legacy.

Con is French slang for vulva. This will inevitably lead to categorical jokes about co-con aka... the problem we started with.

Apparently they can survive nuclear explosions.

(Tadeusz) Just like with the Chapon proposal, this one seems to go against Marketing 101.

An animal I like, tho it is not super-french, but seems nice for a Coq++ and sounds pretty cool. "The Cobra proof assistant"

This is Coq's twitter handle, and actually could be a good short-term replacement, but I dunno how it sounds for native speakers.

This is "coq" in Esperanto. It is onomatopeic for the sound of the chicken and happens to be the name of the Gorilla that could speak the language of signs. This proposal is keeping the same name, but writes it and pronounces it in a hopefully language neutral form. It is not too far from the original, still short, and easy to explain. Apparently .k is not taken (good bye Verilog).

(Tadeusz) Even if one ignores that it apparently means “vagina” in Haitian Creole (as pointed out by Lélio), the fact that phonetically, it's apparently slang for “a communist” in French (as pointed out by Matthieu) should be a non-starter, regardless of one’s political beliefs, the attitude towards governing elites, big corporations and banks (negative on all accounts in my case). Many people, many ethnicities wouldn't appreciate at all if Coq's developers deliberately chose a new name with such connotations. And, if I may say so, the French academia, having brought up a monster like Pol Pot and having hosted for decades the most Stalinist variant of a communist party west of the Iron Curtain, should show just a little bit more sense on this issue. Perhaps even more than on the issue of forcing Anglophones into penis jokes.

Sounds like bawk (what anglophone chickens say).

After Paul Lockhart (the mathematician)

(Andreas: In certain Asian pronounciation, "Rockhard", and we are back to the initial problem.)

The Roc is a giant bird from mythology.

One thing I always like to play with is just adding a constant to the value of each letter, base 26.

For Coq this generates some fantastic other inappropriate ones (Frt would likely be pronounced “fart,” and Dpr “diaper”) but some OK ones like “Mya” and “Ugi” and some really amazing ones like “Seg” and “Amo.” The first one of these leads to delightful puns when things are “not Seg’s fault” and the second is, y’know, “We love Amo,” this Latin root connected to romance.

Keep the command line tools the same, keeps the french heritage, is tangentically related to its origin since it's from a very common flower in Europe. The logo becomes quite obvious too and it is a documented word in english too for a [shade of red](https://en.wikipedia.org/wiki/Coquelicot , the spelling might seem difficult but it's reasonably easy to pronounce in english as "caw cli cawt".

Other languages can abbreviate it to coq in french or `こうく｀in japanese

It's a nice name, but already used: http://coquelicot.saclay.inria.fr.

I quite like the invented word "grok" whose meaning is related to Coq. As the word "grok" might have already be in use (and might be difficult to trademark), we might consider to use the word "Groq".

Proof Assistant Formerly Known As "Coq"

That would work well in presentations: it amounts to a name rather than some such phrase as 'The proof assistant'.

(Tadeusz) It is actually an interesting way to address the awkwardness of “... Formerly Known As Coq” head-on. The subtext of a crazy-yet-talented rock star is also rather entertaining.

• The sound a baby chicken makes (maintains Coq:Rooster reference)
• To take a look at something, either playfully or through a small window (the lens of proofs).
• Short for "people", in a very friendly way (e.g., hanging out with my peeps)
• Can backronym to "Proof Engineering and Extraction Program"
• tasty marshmallows everyone loves, multicultural (Easter candy made by a Jewish confectionary)

Drawback: peeping tom means voyeur. I hope no coq user is called tom / thomas.

Drawback: "peep" also has a strong sexual connotation in French. Should really be avoided.

• Sounds like "rigor". You could drop the "De", my French isn't good enough to know if that makes any sense or not.
• Suggests formalization should obviously be used.
• Irritating to spell for Americans.
• Definitely French.

Drawback: Too jokey.

• The sound reminds that of Coq
• It's still French but easily understandable and pronounceable by non-French speakers
• I don't see opportunities for lame jokes
• It does not have an obvious meaning

Dinosaur discovered in France https://en.wikipedia.org/wiki/Pyroraptor

Dinosaurs are similar to chicken.

It sounds cool.

• Sounds like "calculus" as in "calculus of constructions".
• Has "Coq" as prefix.

• Latin for "I think"; reference to Descartes's "cogito, ergo sum"
• "Cog" has to do with machines.
• "Cog" kinda sounds like Coq, and the g could evoke Gallina.
• "Cog: A coq with a cough." (i.e., the French pronunciation of Coq when one's nose is blocked.)
• Coq General and Interactive Theorem Opener

• Portuguese for "Flight", what a 🐔 cannot do.
• Think beyond.

• Collection of roosters in Portuguese.
• Similar to French slang for "to have an erection".

• The letters used by amateur radio operators to indicate they want to talk with another operator. I suppose it came from "seek you". The English and French pronunciations would differ, there's the charm. Wikipedia notes: "The letters CQ, when pronounced in French, resemble the first two syllables of sécurité", which is a slang way of saying "Social Security" (Sécurité Sociale).

Substring from Coquand.

• leave the official name unchanged, but allow an alias, taken from one of the suggestions above. Then bad puns can be avoided with minimum disruption to the community. By the way, this is why Puritans invented the word "rooster".

As in pure functional programming and refuses to say "Coq". Although, it does seem that puritanism can have side effects.

This is the way.

A clever respelling of Korean "꼬끼오 Kkokkio", an onomatopoeia for cock-a-doodle-doo.

• Contains "coq" as a prefix.
• Not only related to birds but also roosters.
• At the time of writing, Google returns about 30 results, all seem harmless. Probably no cognates as well.

(Dan) I like this name, especially the rooster connection :) Albeit I am not sure how to actually pronounce it correctly.

• Alternative spelling: Coqio. This will remind Danes (and maybe other Scandinavians) of the popular chocolate milk Cocio
• (Guillaume) I have the domain name http://coq.io/ , which is also the name of a project to encode IOs in Coq (I can leave the domain name if chosen)

Another bird in the Galliformes order which is of some national pride for the French, historically important (e.g., Pheasant Island), and generally well-liked.

https://en.wikipedia.org/wiki/Freedom_fries

• Can be read as a shortening of “Calculus of Constructions”.

• Can also be read as “Calculus of [Thierry] Coquand”.

• Sounds similar to “calculate” and “Calculus”.

• Most domain names seem to be taken.

  (Théo Zimmermann) I don't think we should worry about domain names, because we'll likely want to keep using a subdomain of inria.fr.

• (Tadeusz) There is already a conference under this name:

  https://www.coalg.org/calco-mfps2021/calco/

• Sounds a bit like “calque”.

A "Q" from the end of Coq with a combinator that goes both ways. Could be used in verb form: "I Qiff formal proofs".

A mythical, majestic bird, that gets re-born from its ashes. (Also the name of a nuclear reactor near Orange, France)

Simply because it is about checking .v files!

Let us assume that μ is a function of q; It's upto you to decide what those variables mean. It sounds like calculus but I don't know how much it relates to logic or proof. No way to pronounce as a word, must pronounce it letter by letter. "I am working on mu-dee-que" doesn't seem to have any bad connotations, at least to me. I don't know French; thanks for teaching us vulgar/offensive French words.

Means "Ce Qu'il Fallait Démontrer", i.e., Qed in French.

(An appropriate accompanying logo might be harder to come up with)

Justification: Not 'playful' (technical/'boring', even). Not offensive. Distinctively French.

For the francophone user, the meaning is clear, and is more than faithful to any intentions as regards theorem proving (*). It also is distinctively/decisively French, so national pride need not be diminished in this signature gift of INRIA funded research to the world. Nor should there be any anxiety (I hope) about any (perceived) anglophone hegemony in any proposed renaming (even if it's a native English speaker making the proposal ;-))

For the non-francophone user (I hope!), the name is a 'blank' signifier, even if (perhaps) a mouthful to say. But as we have all without (much?) difficulty incorporated 'xkcd' as a word/enunciation into our shared vocabulary, I don't, at first blush, see why this proposed name should be any worse.

If one feels the need to spell it out in words, either do so in French (good practice; appropriately honouring cultural legacy etc.), or say something like "CoQuand's Functional (language of) Demonstration" (So that Thierry's name be thereby retained as a legacy, as many seem to wish to do in discussing/justifying/explaining the old name)

(*) But perhaps the old-timers like myself who remember the various iterations of the 'QED' manifesto might be upset; but I don't think we should be. After all, mathematical custom and practice makes 'CQFD' and 'QED' cognate, even though grammatically/semantically they function entirely differently. The system, and its proof scripts, are what 'furnish the demonstration'.

The Calculus of (Inductive) Constructions would be the calculus of the system :-) So it would be "the Constructions system", "the Constructions proof assistant," etc. An advantage is that the word is the same in French and in English.

For "Constructive vernacular".

Only one letter difference from Coq.

Similar to the CPA / Copa proposal above but as a French acronym.

It's also a well-known Parisian fashion brand.

(Guillaume) This also means armoured personnel carrier in military jargon https://en.wikipedia.org/wiki/Armoured_personnel_carrier

Also a rooster, and a famous one at that. Character in the Medieval Reynard cycle and perhaps more famously still, The Canterbury Tales.

Advantages:

• Bereft of any negative connotations or unfortunate false cognates as far as I'm aware
• (Norman) French
• still a rooster!

Disadvantages:

• bit of a mouthful

• Similar to old name
• Maintains the reference to Thierry Coquand
• The sound a rooster makes (when it's not crowing)
• Doesn't seem to have any innapropriate connotations or conflicting meanings.
• Sounds like 'toque' (Dutch word for jockstrap)

• https://en.wikipedia.org/wiki/Rococo
• The French architectural design style that abandons the cleanliness of classical styles (as Gallina abandons classical LEM)
• The architectural fusion of nature and East Asian themes (Coq fuses Gallina, Ltac, Ltac2, notations, ssreflect, vernacular)
• Still retains "Coq" - can emphasize this by misspelling it as "Rocoqo"

Not really a good name, but it retains one other feature of the Coq, it chases the night and brings about the daylight, which can be a symbol of knowledge.

• Pronounced 'cocker', another animal
• 'R' for 'R'evival
• Very close connection to the existing name

• Pronounced "cok-eight" in English.
• Refers to the current 8.* version of Coq.
• May bump to Coq9 in the future.

French for boiled eggs (wikipedia), eaten inside the shell. Contains 'egg' and 'coq' (really it's 'coque' meaning 'shell').

Could mean both Coq version 9 or the new Coq.

(Tadeusz) A nice idea, especially that I’ve been wondering for how long Coq is going to stay stuck on 8.x. It’s a bit like with MacOS stuck for two decades on 10.x, but even Apple finally took the plunge. Renaming could be a good idea to try some changes you’ve been always thinking about yet afraid of (such as removing modules from the kernel?). To ensure that “neuf”/“n'œuf” doesn’t get dropped, you could try “Coq9” (added).

A cute marsupial indigenous to parts of Australia. It sounds a bit like "Coq", and retains a distinctive "q". In English, it's fun to say. There are a couple of other software projects that use this name, though.

When trying to add a letter to Coq to alter the pronunciation, I found that Corq sounded quite ok. I think it is similar enough to Coq and connected either to Ireland or wine bottles. After a google research I've also seen that it seems an acrononym for "chaotic organized rich of qualities".

It's a small coq.

• ANC = ANC is Not Coq
• Acronyme auto-référent, à la mode GNU (GNU is Not Unix).

• QED = Quod Era Demonstratum
• (see also the proposal above for CQFD)

• En référence au grand savant, mathématicien, philosophe.

Another bird, was used to point out when something was wrong in the mines, also studied for its language/song.

After Grigori Perelman

• Closest English and French words are "concrete" and "concret", with no bad connotations.
• It starts with Coq
• Doesn't seem to be in use

Meaning "proud" in French. Reference to the phrase "Fier comme un coq" meaning "proud as a rooster".

• Pays homage to LₐTᵉX.
• Does not rhyme with croak - I am sorry, it just doesn't. The "q" must be articulated as a voiceless velar fricative (e.g., the ch in loch) or you will not be listened to.
• Equally and universally uncomfortable to typeset and pronounce.
• If you have bad vision like most computer users, you will not notice the name change due to the visual acuity required to detect the additional squeezed-in letters. This is in fact the same reasoning that Leslie Lamport used when naming his tool LaTeX after Tex. The results speak for themselves, and soon Cᵣoᵃq will be as successful as LₐTᵉX.

Self-justifying.

Because the experience is delicious.

Théo W: As a French speaker, I think the first thing that comes to mind is dog/cat food, or a dog's name.

Alouette (a lark, a nice bird) + Huet

• Another rooster-like bird 🐔
• The French pronunciation is close to the English one
• I don't know if there are any negative connotations in French or English

• Rhymes with Coq
• Preserves French heritage of project
• Has fun sandwich connotations (croque monsieur/madame) - good for logos?
• No known negative connotations as a native English speaker

Linked with the rooster's sing

• Short for équivalent/equivalent
• Refers to mathematics
• Doesn't seem to have any inappropriate connotations or conflicting meanings.
• Doesn't seem to be in use

(Dmitry Borzov) Reason language already exists