The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

Dear Benjamin, Derek, contributors to the discussion,

As indicated by Matthieu, the current discussion started from wrong
assumptions. The ICPRAM/ICORES/ICAART mails which pushed Benjamin to
initiate the discussion were sent by non-subscribed senders and
arrived in the hands of the moderators.

Altogether, there are 5 people with moderation rights, but, out of
habits, two are effectively moderating. One moderator is taking in
charge to systematically forward Coq related messages from
unsubscribed senders (unless this is a duplicate or similar reason)
and I'm dealing with the rest of the messages.

In general, I'm forwarding the announcements related to our
communities in a large sense (type theory, formal methods, ...),
and/or with Program Committees including people from our communities,
and/or which I feel may be of interest for some readers.

Evaluating whether it is worth to re-send an announcement is
delicate. Sometimes, not knowing what decision to take, I'm even
looking at what decisions other public lists such as U-Penn's TYPES,
or the lists for Isabelle, or Agda, or OCaml are taking.

Maybe was I today in a favorable day. In any case, I shall accept the
criticism that these 3 announcements are at the margin of the Coq
topic and only loosely (potentially) connected to formal proofs. Are
they spam? Are they fake? My quick evaluation was that there were not,
but I may be wrong and I'd be ready to revise my judgment. After all,
Coq is not exclusively used by people from our "usual" communities, so
if some people from loosely connected communities evaluate (assuming
good faith) that Coq is a potential valuable tool for their community,
I don't see why they should be (at least systematically) excluded.

Then, how to reformulate Benjamin's question based on this new
information?

- Is the non-moderation of the list to subscribers a problem?

  Moderating each message would require more man power and would
  induce delays in the communication. My own feeling is that the
  current ratio signal/noise is rather good. Even if not everyone is
  interested in any "philosophical" question, or in any beginner
  question, or in any subscriber-sent announcement already sent on 3
  or 4 other mailing lists, it is relatively easy to select what is of
  interest for each of us.

- Should Coq-club stop to be about announcements not strictly related
  to Coq?

  Then announcements for the Coq workshops would be ok, but no more
  announcement for general conferences or workshops of our
  communities, no more announcements for summer schools without a
  class on Coq, no more job offer not explicitly mentioning Coq...

  After all, several of us receive such announcements in multiple
  copies and an extra announcement on Coq-club may not be needed to
  reach more people?

- If non-strictly-Coq announcements are still welcome, should the
  policy on announcements from non-subscribers be different?

  For the record, in the recent weeks, announcements from
  non-subscribers were sent for CICM, SYNACS, MPC, iFM, ACL2, HOPE,
  VTSA, ... and I forwarded the mails. If we leave aside the 3
  contentious announcements sent today, is the moderation limit not
  put at the right place?

Incidentally, I would be curious at knowing what policy TYPES/announce
or Haskell, or Isabelle, or Agda, ... are adopting for moderating
conference announcements.

Best,

Hugo

On Fri, Jun 22, 2018 at 10:03:50PM +0200, Matthieu Sozeau wrote:
> Actually, posts are moderated! We just ought to be stricter on 
> announcements.
> Le ven. 22 juin 2018 à 20:28, Derek Dreyer 
> <dreyer AT mpi-sws.org>
>  a écrit :
> 
>     I thought of it, but didn't imagine the mailing list management would
>     support such a feature easily.  If it does, then sure.
> 
>     Derek
>     On Fri, Jun 22, 2018 at 8:26 PM Clément Pit-Claudel
>     
> <cpitclaudel AT gmail.com>
>  wrote:
>     >
>     > On 2018-06-22 14:18, Derek Dreyer wrote:
>     > > Another idea would be to not moderate posts but have a stronger
>     > > vetting process for determining who has the right to post rather 
> than
>     > > just allowing anyone.  However, this might have the effect of
>     > > discouraging newbies with real Coq questions.
>     >
>     > Many online forums moderate the first few posts of each new user.  
> Could
>     this work on coq-club?
>     >
>     > Clément.
>