The Coq mailing list

[Guillaume Claret <guillaume AT claret.me>]

I am surprised by the amount and I feel it is nice that there are many 
names propositions in https://github.com/coq/coq/wiki/Alternative-names 
I dislike Coq being associated to the English meaning but this seems a 
common idea. Being the international language, I think this is something 
to take into account, especially if that can help.


Guillaume


The 04/07/2021 at 03:18, Conor McBride wrote:
> I would also observe that this entire public discourse is data input to a 
> discipline
> known as "cultural policy research".
>
> This is not a disposable conversation.
>
> Good luck, future comrades
>
> Conor
>
> > On 7 Apr 2021, at 02:09, Cyrus Omar <comar AT umich.edu> wrote:
> >
> > 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