The Coq mailing list

[Beta Ziliani <beta AT mpi-sws.org>]

About the logo: as I said on Twitter, it is best if it can be used in multiple places, with multiple sizes. So it is best if it is kept simple, like the current one.

About the name: I agree that we could try spelling its name. This means we should start capitalizing it (COQ). When asked we can say "Calculus Of Quantifications" (joking!).

Best,

Beta

On Tue, Apr 6, 2021 at 8:53 AM Thorsten Altenkirch <Thorsten.Altenkirch AT nottingham.ac.uk> wrote:

Actually this may work very well. If the controversy is picked up by the media this may be a good way to make people aware of the existence of tools like coq. Negative attention is better than none.

 

I am going to call the tool coq and not see-oh-quiche but everybody is welcome to experiment as they like.

 

Thorsten

 

 

From: <coq-club-request AT inria.fr> on behalf of Benjamin Pierce <bcpierce AT cis.upenn.edu>
Reply to: "coq-club AT inria.fr" <coq-club AT inria.fr>
Date: Tuesday, 6 April 2021 at 12:36
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Why is the Coq logo made to look like a penis?

 

Clinging to a name that was intentionally chosen to give offense doesn't seem like a great idea for a group that is trying to promote good ideas in the larger community: Don't people already have enough reasons to ignore us?  :-)

 

Personally, I'm going to experiment with saying See-Oh-Queue and see how it wears; this seems like a low-cost change that could be implemented by some of the community without agreement from all.  But if people are up for discussing a whole new name, that's fine too.  I like several that have been proposed in this thread.

 

As for the logo, it seems no one much cares for the current one (me included).  

 

    - Benjamin

 

On Tue, Apr 6, 2021 at 6:57 AM Thorsten Altenkirch <Thorsten.Altenkirch AT nottingham.ac.uk> wrote:

I agree. Maybe I am getting old but I always enjoyed the cheek of choosing a name which may upset some people. I also enjoyed telling the story about Gerard Huet giving a talk about the zipper and its verification with coq. I do remember that Ursula Martin was rather upset. Certainly this was provocative. It seems nowadays everybody is offended by something. I guess this is the culture now. Not necessarily something I appreciate. I think coq is a brand name and it would be a bad idea to change it. Also it never occurred to me that the logo had anything to do with a penis. Isn’t this in the (dirty?) mind of the beholder?

Thorsten

On 06/04/2021, 10:51, "coq-club-request AT inria.fr on behalf of Guillaume Claret" <coq-club-request AT inria.fr on behalf of guillaume AT claret.me> wrote:

    I am strongly against changing the name.

    Le 06/04/2021 à 11:49, Paolo Torrini a écrit :
    > Since there's already an *important* distinction between language
    > (Galllina) and prover (Coq), wouldn't it actually make sense to
    > introduce a new name to designate the whole lot?
    >
    > Say, one could simply abbreviate Gallina-Coq to Galliq, or call it
    > Roost, or anything else appropriate. That would save from explicitly
    > changing name, while defusing the anglophone issue - and it might even
    > help to make things more precise.
    >
    > Best,
    >
    > PT
    >
    > On 06/04/2021 11:04, Derek Dreyer wrote:
    >> Personally, I would support changing the name *and* the logo.
    >>
    >> The root problem is the name -- I rather doubt the logo would be
    >> controversial if it were not for the name.  As is well known, the name
    >> was deliberately intended partly as a joke, to provoke people -- it
    >> has succeeded in that regard.  But mostly at this point it is just
    >> embarrassing to a lot of us, and probably exacerbates the gender
    >> disparity in Coq users.
    >>
    >> I have heard people say that it is hard to change the name.  I agree,
    >> it is hard, but that doesn't mean IMO that it's not worth exploring.
    >> I bet that many Coq users would be very open to a name change if a
    >> catchy new name were proposed by the Coq team.  I would, for one.
    >> (And I'm happy to help brainstorm about new names privately if anyone
    >> cares to have that discussion.)  Of course, perhaps I am wrong: it
    >> might be worth polling Coq users about whether they would like to see
    >> the name changed, if that has not been done already.
    >>
    >> That said, if there is not sufficient support for changing the name, I
    >> would at least support changing the logo to something that is less
    >> open to interpretation and more clearly resembles a normal rooster (or
    >> even Ilya's steampunk rooster).
    >>
    >> Best regards,
    >> Derek
    >>
    >>
    >> On Mon, Apr 5, 2021 at 6:49 PM James R Wilcox
    >> <jrw12 AT cs.washington.edu> wrote:
    >>> I had never noticed this before, despite apologizing for the name of
    >>> the proof assistant to my students for many years. This year, I had a
    >>> student point out to me the
    >>>
    >>>> flesh-colored logo with what looks like a mushroom top
    >>>
    >>> and now I can't unsee it.
    >>>
    >>> Isn't it time for a new logo?
    >>>
    >>> James R. Wilcox
    >>> University of Washington, Seattle




This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment.

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored
where permitted by law.

This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment. 

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored 
where permitted by law.