The Coq mailing list

[Théo Zimmermann <theo AT irif.fr>]

Hi Zoe,

Not really. The introduction was simply entirely rewritten and
simplified. We could reintroduce Gallina in the sentence "The first
part presents the specification language of Coq, that allows to define
programs and state mathematical theorems." (which would become "The
first part presents Gallina, the specification language of Coq, that
allows to define programs and state mathematical theorems."). Or we
could put even more emphasis on it that there used to be by changing
the first sentence to "This is the reference manual of Gallina / Coq.
Coq is an interactive theorem prover and Gallina is its specification
language.". This was the kind of thing I was thinking of when asking
my question earlier.

Théo

Le mar. 6 avr. 2021 à 11:55, Zoe Paraskevopoulou
<zoe.paraskevopoulou AT gmail.com> a écrit :
>
> Relevant to this discussion, I would like to point out that Gallina (which 
> was a nice alternative name to use) is no longer mentioned in the reference 
> manual as the official name of the specification language of Coq 
> (https://coq.inria.fr/refman/ vs 
> https://coq.inria.fr/distrib/V8.11.2/refman/), which is confusing.
>
> Was this a deliberate decision? I would like to see Gallina in the front 
> page of the manual again.
>
> Best,
> Zoe
>
> On Apr 6, 2021, at 12:04 PM, Derek Dreyer <dreyer AT mpi-sws.org> 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
>
>