Important note: if you had never heard of Coq before reading the article on theregister.com, then your opinion on this matter is probably not relevant to us. Please consider staying out of this process, thank you very much!

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 was created to collect ideas for alternative names or alternative pronunciation strategies. We intend to run 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).

The ideation phase is now over, but if you still want to add to this page, do it in the "Late ideas" section.

The page https://github.com/coq/coq/wiki/Implications-of-changing-the-name gathers expected implications of changing the name.

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.

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.

Advantages:

• From one Anglophone 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. Unless it is written couq (u for universes). But then, we actually need to change the names of the tools.

Expanding the name to one that sounds very French (Le Prouveur 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. This works the same way as the brand le coq sportif.

Advantages: honors the French heritage and promotes more diversity.

Disadvantages: could still risk being shortened to "Coq" in conversation, but we could recommend shortening to LPC instead.

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: same as above

Issue: Couldn't be shortened to LCF, which would be confusing. The recommended acronym could be CF.

Short version of the above proposals.

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é?

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

A fitting name for a tool used to assist theorem proving.

Warning: could also be seen as a reference to cockfights, which an unethical practice.

(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

(Théo) For every joke with Coq, there already seem to exist a vim extension (Coquille, Coq au vim, Coqpit). But actually, nowadays, the most well-known Coq vim extension is Coqtail and I guess we could ignore the other ones.

A pretty bird that never upset anyone. And "p" for proof (could be interpreted as "proving with Coq", "proofs in Coq" or similar).

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

Note both Pcoq and PeaCoq are the names of graphical interfaces to Coq (see https://www-sop.inria.fr/lemme/pcoq/ and http://goto.ucsd.edu/peacoq/). The former is no longer maintained, while the latter might still be.

Since it was already said that Coq was named after Coquand.

This has precedent, for example in programming languages that are named after persons, such as Haskell, Pascal, Ada, etc.

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.

Disadvantage: anglophone outsiders who have never heard of Coq and Coquand can mispronounce "Coquand" as "Coq and", which has led to several commenters on theregister.com joking with "Coquand Balls". Nevertheless, this would still avoid the main issue with the current name which occurs when outsiders hear someone talk to them about Coq (as long as the person talking knows how to pronunce "Coquand" correctly).

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"

Calculus Of CORrect Inductive COnstructions

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

The second spelling is not an acronym, just a reference to the rooster's crow in French.

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.

Advantages: retains the original name, 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.

The monster begot by Coquand and hatched from Coq’s egg. The glance of its eye suffices 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

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

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

It's a small coq.

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

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

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

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

Note: There exists an unreleased, under development programming language called Roc (named after the mythical bird) - https://roc-lang.org

Gallo is the Italian word for rooster (and also a somewhat declining Eastern Brittany language, https://en.wikipedia.org/wiki/Gallo_language)

It would be a nice dual Gallina (the Italian word for chicken).

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

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

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

(Théo) Sounds closer to garlic than phallic.

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

the Calculus Of Inductive Qonstructions

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

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 )

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?

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.

Another translation of chicken

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

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.

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.

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)

After Paul Lockhart (the mathematician)

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

As was argued elsewhere, there isn't an actual problem with the phrase "rock hard" which is not necessarily associated to a penis.

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

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

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

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

After Grigori Perelman

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

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

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

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!

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.

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

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.

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 acronym for "chaotic organized rich of qualities".

Reason for discarding: In French, it sounds close to "cocu" which is a deceived husband.

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

Reason for discarding:

• This is not the French pronunciation: French has no "G" sound
• Seems awkward in both French and English (Benjamin Pierce).

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.

Reason for discarding: would still end up being shortened to "Coq" in conversation, and the problem would therefore not be solved.

Reason for discarding: The Portuguese cognate "galinha" can be offensive (it means "promiscuous person", usually a woman).

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

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

Reason for discarding: would give the impression that American Puritanists and American imperialism have won. Also, too close to the "Rust" language.

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.

Reason for discarding: sounds too close to phallus.

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.

Reason for discarding: risk creating confusion between Gallia and Gallina

Sounds like "goal", keeps French connotation?

Reason for discarding: "Gaule" can be definitely used to mean "erection" in French.

A short portmanteau of Gallina + Coq.

Reason for discarding: awkward to pronunce in French

Another short portmanteau of Gallina + Coq.

+: A minimal diff from Coq.

Reason for discarding: awkward to pronunce in French

Reason for discarding:

• (Jasper Hugunin) 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

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.

Reason for discarding:

• same problem of confusion than for Gallina
• (mmalter) It's the name of a bank in France

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

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

I would disagree with discarding the proposal based on the Russian slang point. The word seems to be used extremely infrequently and enjoyed its limited popularity in 80s-90s and 00s, then waned completely. I did not know this interpretation as a native speaker, and quick survey of my contacts (age 20-40) from Belarus and Russia revealed that they didn't know it either, or encountered it in old books or from their grandparents. It's safe to say that this interpretation will not be the first, second or even third association for the vast majority of Russian speaking folks. It is therefore unwise to discard this proposal due to mere existence of such interpretation. I believe that coqi is a terrific name due to its simplicity and closeness to the original. I suggest that the decision be amended. (AK)

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)

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.

Reason for discarding: 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.

Reason for discarding: In French, Coquina is liable to be perceived as a cognate of coquine which can have sexual connotation.

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.

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

Reason for discarding: can have a violent meaning in some parts of Latin America.

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.

Reason for discarding: Offensive in French (is it though?).

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

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

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

Reason for discarding: hard to pronounce in English.

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

Reason for discarding: alternative proposals for making Coq sound more French are available and are more specific to a theorem prover.

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

Reason for discarding: not French enough (compare to the alternative Cocorico / Coqorico).

Sounds like bawk (what anglophone chickens say).

Reason for discarding: see above.

Reason for discarding:

• There's a programming language with that name.
• Too close to the C Compiler.

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

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?

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

A strong monster from the nethack games.

https://nethackwiki.com/wiki/Cockatrice

Reason for discarding: seems strictly inferior to the Coqatrice proposal, which would allow keeping the name of the tools.

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

Reason for discarding: naming Coq documents doesn't resolve the issue at stake.

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.

Reason for discarding: 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.

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.

Reason for discarding: 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.

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

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

Reason for discarding: too bland

Reason for discarding: raises strong reactions (see reaction by Tadeusz below). → His reaction was against the name “coco”, and doesn’t affect koko or coqo. Should we split this proposal into three (koko / Coqo / coco) instead?

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 nickname and common name. It is also a shorthand for communist, but this is not the first meaning that comes to mind.

Koko 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). → It is actually taken by [https://kframework.org/] for K files. There is a extraction from K to Coq, so there might be some conflicts (but they would be similar than the ones of teams using Coq to work with circuits).

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

(Martin Bodin) The meaning “a comunist” for “coco” in French is extremely rare: be assured that Disney and Pixar would never have translated their movie [https://fr.wikipedia.org/wiki/Coco_(film,_2017)] like that if there were any strong association with comunism. I would be slightly more concerned by the fact that in portuguese children language, “coco” is a slang for defecation (at least in some parts of Brazil). I don’t know whether this is the reason why they changed the title in Brazil to “Viva: A Vida É uma Festa”. It’s a minor concern, but technically still a negative association.

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.

Reason for discarding: No actual proposal.

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

Reason for discarding: already used by a widely known Coq library 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".

Reason for discarding: too close to "grope"?

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.

Reason for discarding: too hard to pronounce.

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

Reasons for discarding:

• peeping tom means voyeur. I hope no coq user is called tom / thomas.
• "peep" also has a strong sexual connotation in French. Should really be avoided.

• Collection of roosters in Portuguese.

Reason for discarding: 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.

Reason for discarding: "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.

Reason for discarding: strictly inferior to 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".

Reason for discarding: when people use a name inside the community, they will forget switching when going out. Also problematic for searching.

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

Reason for discarding: joke.

This is the way.

Reason for discarding: joke.

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

Reason for discarding: joke.

Reason for discarding:

• there is a conference with this name
• sound similar to CoCalc which is a platform used by many computational mathematicians

• 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”.

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.

Reason for discarding: too complicated.

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

Reasons for discarding:

• It's also a well-known Parisian fashion brand.
• (Guillaume) This also means armored personnel carrier in military jargon https://en.wikipedia.org/wiki/Armoured_personnel_carrier

• Similar to old name
• Maintains the reference to Thierry Coquand
• The sound a rooster makes (when it's not crowing)

Reason for discarding: Sounds like 'toque' (Dutch word for jockstrap)

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

Reason for discarding: sounds like "cocard" in French.

(Martin Bodin) It’s actually how we named our Coq formalisation of the R programming language, but I guess we can easily update this name too if it’s any trouble.

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.

Reason for discarding: There are a couple of other software projects that use this name.

• ANC = ANC is Not Coq

Reason for discarding: but it is.

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

Reason for discarding: joke.

Because the experience is delicious.

Reason for discarding: 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.

• 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

Reason for discarding: it's an almost-homonym of "croak", which is slang for "die", which is pretty negative

Reason for discarding: (Dmitry Borzov) Reason language already exists

• Bonus point: Keeps the French heritage: will confuse Americans on correct pronunciation. French speakers will thus be able to point out it's pronounced "pouleh" not "poulette".
• No known negative connotations as a native English speaker.
• Literally means "chicken" in French, whereas Coq means "rooster".
• Has the slang meaning of "cop" in French, and, indeed, this reflects the experience of the proof assistant as some kind of gatekeeper or police force stopping bad proofs from being accepted.

• Wouldn't that be a great name for a proof-assistant?
• Which keeps the first two of three letters of coq!
• Bonus: contains the word 'cop' as a truth-gatekeeper
• Bonus: not an acronym with multiple potentially dangerous meanings
• Bonus: not reserved in the Wipo brand database

• Coq in French slang means cocaine. Hasch means in Englisch hashish, which is also some substance that makes you addictive.
• There is this song "Dans mon H.L.M." by Renaud Pierre Manuel Séchan, where it says: "La fille du huitieme, le hasch elle aime"
• Hasch has some resemblance to hash, which is also used in computer science a lot and therefore would stick well in people's minds.

• Very short extension of existing name, but new name doesn't resemble any "difficult" words in English

Reason for discarding (same as co-Q): In French, it sounds close to "cocu" which is a deceived husband.

• Because the organized whole is truly greater than the sum of its individual...libraries, contributors, plugins...

• Because it is!
• Easy to pronounce, at least in English and French.

Name for the "Cal(culus of) i(nductive) co(nstructions)".

Has the benefit of easily suggesting a cute mascot. Compiler could be abbreviated to clc.

• On the usual french keyboard layout A and Q are switched compared to english/american keyboard layout.
• COA stands for Certificate Of Authenticity, which sounds pretty serious!

• close to coq
• Calculus Off (All) Construction Hierarchies, or whatever better acronym.

### COR (COq Renamed)

• R is the next to Q in alphabetical order.
• CORE would also work but not sure we want such a common word.