5 ms·

Maybe they should rename it?

yaantc 12y ago
Honi soit qui mal y pense ;) A coq is a rooster in French, as can be seen from the coq logo. One of the author is called Coquand, the rooster is the emblem of France (where it comes from) and the coq language is called gallina (rooster in latin). So it's a multi levels pun, and likely here to stay. There's a grand tradition of goofy names in open source, but in this case I feel it's safe to say it won't be the main barrier to mass adoption.
- wk_end 12y ago
  It's also, IIRC, based on a logical model called the Calculus of Constructions - or CoC, for short.
  - bch 12y ago
    > It's also, IIRC, based on a logical model called the Calculus of Constructions "Calculus of Inductive Constructions" (https://coq.inria.fr/about-coq https://coq.inria.fr/about-coq)
    - Cederfjard 12y ago
      From your link: > Coq is the result of more than 20 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. In 1991, Christine Paulin extended it to the Calculus of Inductive Constructions.
    - tel 12y ago
      The CoC provides the basic framework for Coq, while the Co(I)C or even the Calculus of (Co)-Inductive Constructions provides a dramatic extension in power and expressivity necessary for "real" programming in Coq.
bob917 12y ago
I am both amazed and ashamed at some things I've used coq for.
vegabook 12y ago
Sometimes a cringe-inducing name is great for visibility and marketing. See "Wii", even "iPad"...
Cederfjard 12y ago
Is it really an issue though? Don't restaurants have coq au vin on the menu where you're from?
bnegreve 12y ago
This issue is addressed in the FAQ: https://coq.inria.fr/faq?q=node/16&som=2#htoc4 https://coq.inria.fr/faq?q=node/16&som=2#htoc4
clarus 12y ago
Actually this is funny, because "bit" means in French the same thing as "Coq" in English. Probably to be fair we should debate about renaming "bit" also :) (or not).

Honi soit qui mal y pense ;) A coq is a rooster in French, as can be seen from the coq logo. One of the author is called Coquand, the rooster is the emblem of France (where it comes from) and the coq language is called gallina (rooster in latin). So it's a multi levels pun, and likely here to stay. There's a grand tradition of goofy names in open source, but in this case I feel it's safe to say it won't be the main barrier to mass adoption.

wk_end 12y ago
It's also, IIRC, based on a logical model called the Calculus of Constructions - or CoC, for short.
- bch 12y ago
  > It's also, IIRC, based on a logical model called the Calculus of Constructions "Calculus of Inductive Constructions" (https://coq.inria.fr/about-coq https://coq.inria.fr/about-coq)
  - Cederfjard 12y ago
    From your link: > Coq is the result of more than 20 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. In 1991, Christine Paulin extended it to the Calculus of Inductive Constructions.
  - tel 12y ago
    The CoC provides the basic framework for Coq, while the Co(I)C or even the Calculus of (Co)-Inductive Constructions provides a dramatic extension in power and expressivity necessary for "real" programming in Coq.

bob917 12y ago

I am both amazed and ashamed at some things I've used coq for.

vegabook 12y ago

Sometimes a cringe-inducing name is great for visibility and marketing. See "Wii", even "iPad"...

Cederfjard 12y ago

Is it really an issue though? Don't restaurants have coq au vin on the menu where you're from?

bnegreve 12y ago

This issue is addressed in the FAQ: https://coq.inria.fr/faq?q=node/16&som=2#htoc4 https://coq.inria.fr/faq?q=node/16&som=2#htoc4

clarus 12y ago

Actually this is funny, because "bit" means in French the same thing as "Coq" in English. Probably to be fair we should debate about renaming "bit" also :) (or not).