The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

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