The Coq mailing list

[Xuanrui Qi <xuanrui AT nagoya-u.jp>]

Dear all,

First of all, I thank Talia and Kenny for organizing this event and the
Coq team for similar efforts.

I do not understand what this heated debate is all about. According to
my understanding, Talia shared an invitation to an event, which happens
to be somewhat political but certainly related the topic of this list.

At least a handful of calls for participation in events circulate on
this list daily, and many of them are only marginally related to Coq.
Moreover, it is definitely not the case that CfPs of those events do
not contain similar (one might say, "subjective" or "sounds-like-
universally-quantifying") assertions, yet I cannot recall anyone making
a fuss out of it. I cannot see why this post is more problematic than
any of the aforementioned posts.

I don't endorse this "keeping politics out of the list" attitude, but
that isn't even relevant here. According to my understanding, the
original post is not calling for a political discussion; it is no more
than a call for participation. Questions about CfPs, in general, should
perhaps not go on the mailing list where the call was circulated.

-Xuanrui


On Tue, 2020-06-09 at 18:01 -0700, Talia Ringer wrote:
> Here is a constructive proof that this forum has been used in the
> past to announce a meeting to discuss diversity initiatives in our
> research community: 
> https://sympa.inria.fr/sympa/arc/coq-club/2019-02/msg00019.html
> 
> This is no different.
> 
> On Tue, Jun 9, 2020 at 5:56 PM Dominique Larchey-Wendling <
> dominique.larchey-wendling AT loria.fr> wrote:
> > Dear all,
> > 
> > I strongly *believe* that for this scientific community
> > particularly, enforcing
> > the difference between beliefs and proofs is of utmost importance.
> > 
> > To my knowledge, this mailing list has always been about proofs
> > and methods to build them, and because of that, mostly gentle
> > as far as I can remember.
> > 
> > While I can certainly understand the importance of the concerns
> > that
> > are discussed right now, I do not think this is the place. There
> > are plenty
> > of forums to discuss political matters.
> > 
> > Best,
> > 
> > Dominique
> > 
> > > De: "Talia Ringer" <tringer AT cs.washington.edu>
> > > À: "coq-club" <coq-club AT inria.fr>
> > > Envoyé: Mercredi 10 Juin 2020 01:45:05
> > > Objet: Re: [Coq-Club] Shut Down PL
> > > It would help to read the entire thread before responding. I
> > > already addressed that we never intended for there to be an
> > > implicit universal quantifier in there. English is ambiguous and
> > > this was an existential claim. Which Christine has just mentioned
> > > she has constructively proven. I'd say QED, but I have very
> > > strong political beliefs that acting as if proofs are irrelevant
> > > is harmful, so I always use Defined.
> > > 
> > > On Tue, Jun 9, 2020, 4:39 PM Randall Holmes <
> > > rholmes AT boisestate.edu> wrote:
> > > > I don't think it *is* irrelevant to the purposes of this list
> > > > to point out that " We in the global programming languages
> > > > community acknowledge that every institution in our society is
> > > > built on a foundation of white supremacy—and our academic
> > > > systems and research industry are no exception." is a universal
> > > > statement -- and, as the outcome of the discussion reveals,
> > > > false.
> > > > 
> > > > Further, to say that this is false is not to refuse to take an
> > > > anti-racist stand.  I'm not a racist.  I despise racism and
> > > > oppose it in whatever way I can.  But it is false (and deeply
> > > > relevant to what we are all doing) to claim that the research
> > > > enterprise of mathematics and computer science is built on a
> > > > foundation of white supremacy.  Such statements must be firmly
> > > > challenged.  I suspect that people who make them (or chime in
> > > > approvingly when they hear them) often are not really listening
> > > > to what they are saying.
> > > > 
> > > > There are powerful social forces at work (which are
> > > > discouragingly hard to challenge, and sometimes disturbingly
> > > > hard to even catch at work) 
> > > > which make it difficult for black people, and women,
> > > > and members of other disadvantaged groups, to find their way
> > > > into mathematics and computer science research and thrive
> > > > there.  But the obstructions are not essential to the
> > > > enterprise of mathematical, computer science, or even general
> > > > academic research.  The program of mathematical and computer
> > > > science research does not benefit from making it hard for
> > > > blacks and women (and other disadvantaged people) to
> > > > participate.  If we were more diverse...we would still be doing
> > > > the same thing, and doing it better because there would not be
> > > > artificial obstructions to finding the best people to do it.
> > > > 
> > > > Like Christine, I acknowledge that the field is mostly white,
> > > > and mostly male (and, even though I am an elderly white male
> > > > myself) I find this very sad
> > > > and would be happy to work to make the situation better. To
> > > > appreciate this fact is not the same, however, as to believe
> > > > the amazing statement quoted above.
> > > > 
> > > > Sincerely, M. Randall Holmes, Professor, 
> > > > Dept of Math, Boise State University
> > > > The above remarks do not necessarily reflect the official
> > > > opinion of any person or institution.
> > > > 
> > > > 
> > > > On Tue, Jun 9, 2020 at 4:33 PM Tadeusz Litak <
> > > > tadeusz.litak AT gmail.com> wrote:
> > > > > Dear Derek,
> > > > > 
> > > > > On 09.06.20 23:46, Derek Dreyer wrote:
> > > > > >   a broad claim was made that "We in
> > > > > > the global programming languages community acknowledge that
> > > > > every
> > > > > > institution in our society is built on a foundation of
> > > > > white
> > > > > > supremacy—and our academic systems and research industry
> > > > > are no
> > > > > > exception."  I agree with this claim, as I'm sure do many
> > > > > others on
> > > > > > this list.  I guess perhaps you don't, in which case the
> > > > > announced
> > > > > > event is probably not for you.  But I don't see how you can
> > > > > argue that
> > > > > > there is anything unusual or unscientific or "political"
> > > > > 
> > > > > if you don't see what is unscientific or political about the
> > > > > claim you're quoting, or if you believe that this claim can 
> > > > > be legitimately called "assumed knowledge" in any meaningful
> > > > > sense (especially comparable to the lambda calculus 
> > > > > capturing the nature of computation!), we might not share
> > > > > enough basic assumptions (or axioms) to continue this 
> > > > > particular discussion constructively. Which worries me given
> > > > > the respect I have for you otherwise, but c'est la vie.
> > > > > 
> > > > > It's one thing to have a political belief, no matter how
> > > > > outlandish, or how popular. It's another thing to present it
> > > > > as 
> > > > > a self-evident claim that every reasonable person must agree
> > > > > with, in particular as an implicit view of the entire 
> > > > > community. This is precisely the phenomenon described as
> > > > > "moral grandstanding" and you cannot blame people for saying 
> > > > > "not in my name, please".
> > > > > 
> > > > > Whenever this happens, a conflict ensues.
> > > > > 
> > > > > That's all.
> > > > > 
> > > > > t.
> > > > >