The Coq mailing list

[Conor McBride <conor AT strictlypositive.org>]

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