The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

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