The Coq mailing list

[Derek Dreyer <dreyer AT mpi-sws.org>]

I fear that a long multi-word name is suboptimal for branding purposes
and may result in abbreviation.  Le Coq Formel in particular is likely
to be abbreviated as LCF, which might cause some confusion. ;-)

Also, note that in English, people will naturally want to put "the"
before the name of the system, e.g. "the Coq proof assistant".  If
"Le" is in front of it, people will end up writing "the Le Coq proof
assistant", which is quite awkward.

Personally, I think keeping it to a single word (and one which does
not bake in its own definite article) is highly desirable.

Best regards,
Derek


On Wed, Apr 7, 2021 at 4:20 PM nicolas tabareau
<nicolas.tabareau AT inria.fr> wrote:
>
>
> On 7 Apr 2021, at 16:10, Luís Cruz-Filipe <lcfilipe AT gmail.com> wrote:
>
> Thanks, Giselle, for the concise summary of a long discussion!
>
> Point 4 on the pro list matches how I see it: the problem is not the name 
> "Coq", it's the inappropriate jokes that people make based on it. It 
> saddens me that the only way we can find to address this problem is by 
> proposing a name change. While I understand the issues reported by many 
> people on this list, I still find this the wrong approach. Will we be 
> discussing how to deal with people whose surname is Kok (quite popular in 
> some European countries) twenty years from now?
>
> Tadeusz also raises some important points, and I too like the suggestion of 
> going for "Le Coq". It reminds me of Le Coq Sportif, which is also a major 
> French brand that has a rooster as logo and international visibility...
>
>
> As a follow-up on this idea, we have proposed “le coq formel” on the wiki.
>
> More globally, I also think that adding some words around “Coq” to remove 
> the possibility for bad jokes/interpretations in English
> is really something to consider, if not the only way out.
>
> I hope that native English speakers will confirm that it indeed works and 
> prevents people from hearing the silly word in it.
>
> Best,
>
> — Nicolas
>
>
> Best,
> Luís
>
>
> On Wed, Apr 7, 2021 at 3:42 PM Tadeusz Litak <tadeusz.litak AT gmail.com> 
> wrote:
>>
>> The thread is unfortunately named, as the discussion has long ago ceased 
>> to be about the logo, but the idea to rename it
>> has not caught on. Even though there were good reasons to rename the 
>> thread. There is a lesson in it.
>>
>> Anyway, the proposed list of "reasons to keep" does not include the most 
>> important one (apart from massive legacy,
>> second to none in fact). One would need to reformulate point 2. It is not 
>> just about making sense in French. If it is
>> correct that Coq's name appeals to French national pride and that it helps 
>> to get funding and institutional support in
>> France, this is a huge issue.
>>
>> Similarly, it seems incorrect to say "it *was* developed in France". 
>> Unless I'm mistaken, regardless of huge
>> international following and user base, the core development, maintenance 
>> and the entire infrastructure are still
>> provided by French institutions and it's unlikely to change in foreseeable 
>> future. In fact, this institutional support
>> seems to be as important a factor in Coq's survival as its solid 
>> theoretical foundations.
>>
>> So while minor name modifications like "COQ", "Coq au... <French word of 
>> choice>", "Côq", "Le Proveur Coq" or simply "Le
>> Coq" (I actually like that one) seem worth considering and so does the 
>> idea of clarifying the English pronunciation,  a
>> more drastic change could have a few unintended consequences.
>>
>>
>> On 7/4/21 2:52 PM, Giselle Reis wrote:
>> > I think the 100th message in this thread should be a summary of
>> > pro/cons arguments so far.
>> >
>> > Reasons to change:
>> > 1. People are uncomfortable when saying Coq in an English conversation
>> > 2. English is the main scientific communication language
>> > 3. It can be a barrier for people to join the community
>> > 4. It stems from a silly joke
>> >
>> > Reasons to keep:
>> > 1. Legacy
>> > 2. It was developed in France and the name makes sense in this language
>> > 3. We are not changing other English words because they feel
>> > uncomfortable in other languages
>> > 4. We should do better than giggling at silly words (we do not, but we 
>> > should)
>> >
>> > They are, of course, not all weighted the same (that is very
>> > subjective), and I might have missed something, but these are the
>> > points that stood out.
>> >
>> > On Wed, Apr 7, 2021 at 3:39 PM Mario Frank <mafrank AT uni-potsdam.de> 
>> > wrote:
>> >> Dear Jason,
>> >>
>> >> you are right - there are more or less handy alternatives. I could 
>> >> adopt one of those.
>> >>
>> >> Thx for the hint.
>> >>
>> >>
>> >> Am 07.04.21 um 14:22 schrieb Jason Gross:
>> >>
>> >> Dear Mario,
>> >>
>> >>>   I like your idea of using the concrete (specification) language when 
>> >>> communicating about the research/work - and this may work pretty well 
>> >>> in most cases. Sadly, I usually do not work much with Gallina/LTAC/... 
>> >>> but rather on extending
>> >> (the tool) Coq.
>> >>
>> >> If you are so inclined, I think there is a relatively easy fix here, by 
>> >> getting more specific:
>> >> - I work on extending Gallina
>> >> - I work on extending Ltac
>> >> - I work on various tactic languages for constructing Gallina proofs
>> >> - I work on infrastructure for interacting with programs which 
>> >> eventually produce Gallina terms
>> >> - I work on plugins which extend the ecosystem of what can be done in 
>> >> scripts whose primary purpose is to construct Gallina terms
>> >> - I work on integrating new features and abilities into the vernacular 
>> >> language surrounding Gallina.
>> >>
>> >> Granted, some of these are a bit of a mouthful.
>> >>
>> >> Also, this last one reminds me of the fact that there are in fact three 
>> >> languages used in Coq files.  Commands like `Definition`, `Lemma`, 
>> >> `Search` and `Set Printing All` are neither part of Gallina nor Ltac, 
>> >> but instead part of the "vernacular" command language (which as far as 
>> >> I'm aware has no proper name other than perhaps Vernacular or Vernac 
>> >> (the abbreviation used in OCaml code to refer to this part of the 
>> >> language)).
>> >>
>> >>
>> >> On Wed, Apr 7, 2021, 03:34 Mario Frank <mafrank AT uni-potsdam.de> wrote:
>> >>> Dear Cyrus,
>> >>>
>> >>> I like your idea of using the concrete (specification) language when 
>> >>> communicating about the research/work - and
>> >>> this may work pretty well in most cases. Sadly, I usually do not work 
>> >>> much with Gallina/LTAC/... but rather on extending
>> >>> (the tool) Coq. This will hold for many people who implement tools on 
>> >>> the basis of Coq.
>> >>>
>> >>> So, in the light of the fact that there are people feeling 
>> >>> uncomfortable with the biased meaning in different languages -
>> >>> I can confirm the experiences described by some people here - just 
>> >>> avoiding the use of the name will not be a
>> >>> satisfactory solution (to me). It would rather have the flavour of 
>> >>> saying "the tool whose name shall not be said" to me.
>> >>> There are many (good) proposals in the Wiki and I was especially 
>> >>> attracted by "Gallus" as it has a quite matching meaning
>> >>> and also has a (subconscious) connection to Gallina (in my brain).
>> >>>
>> >>> Apart from that, I am happy that this topic is discussed so 
>> >>> extensively. It seems to be necessary.
>> >>>
>> >>> Cheers,
>> >>> Mario
>> >>> Am 07.04.21 um 03:09 schrieb Cyrus Omar:
>> >>>
>> >>> For you, Adam, I think it would be especially appropriate to say "I 
>> >>> write Ltac programs" instead, then. :-)
>> >>>
>> >>> Yes, this would require changing how we speak, in a manner that I 
>> >>> think is quite consistent with our community's values: many of us 
>> >>> quite value being clear about the distinction between a language and 
>> >>> the implementations thereof, even in situations where there is one 
>> >>> primary implementation (e.g. Haskell folks tend to be quite good at 
>> >>> understanding the difference between Haskell and GHC, and of course 
>> >>> the Standard ML community has taken this well to heart.)
>> >>>
>> >>> Cyrus
>> >>>
>> >>> On Tue, Apr 6, 2021 at 9:01 PM Adam Chlipala <adamc AT csail.mit.edu> 
>> >>> wrote:
>> >>>> That doesn't sound right without terminology changes, at least not for
>> >>>> the way I'm used to using Coq.  It's common that more time is spent
>> >>>> writing in the tactic language Ltac than in Gallina.
>> >>>>
>> >>>> On 4/6/21 8:58 PM, Cyrus Omar wrote:
>> >>>>> The first sentence on the About Coq page [1] says "Coq implements a
>> >>>>> program specification and mathematical higher-level language called
>> >>>>> Gallina".
>> >>>>>
>> >>>>> If that is accurate, then I think Gallina seems to be the appropriate
>> >>>>> name to use in conversation as a user of the language, in the same 
>> >>>>> way
>> >>>>> that one says "I write C programs" even if what they are doing
>> >>>>> day-to-day is interacting with GCC, Clang, or CompCert via a
>> >>>>> collection of other utilities, e.g. editors, language servers, and 
>> >>>>> the
>> >>>>> like.
>> >>>>>
>> >>>>> The objection that Gallina is one of several languages associated 
>> >>>>> with
>> >>>>> Coq is the same as the objection that in fact there is a C
>> >>>>> preprocessor language distinct from C the language, i.e. not salient
>> >>>>> in most contexts.
>> >>>>>
>> >>>>> There may still be reason to rename the Coq implementation of Gallina
>> >>>>> (and friends), but it would make it less urgent in that it is only in
>> >>>>> relatively sophisticated company, where crude innuendo is 
>> >>>>> increasingly
>> >>>>> (though not yet universally, I concede) recognized as inappropriate,
>> >>>>> that one needs to mention which particular implementation of a
>> >>>>> language they use or work on.
>> >>>>>
>> >>>>> Cyrus
>> >>>
>>
>