The Coq mailing list

[Tadeusz Litak <tadeusz.litak AT gmail.com>]

On 12.01.20 19:31, Conor McBride wrote:

> Just to say, Tadeusz, I recall enjoying our meeting in Leicester and wish
> you well.

Ditto. It is not just that I enjoyed it. It was an eye opener, which is even 
more important.

While I know that you personally didn't mind, thinking now about Hugo and the rest of the list, I would have used one 
Irish word less replying to your disruption... even as performance art.

Anyway, I am happy that I somehow managed (together with Hugo) to make you  break your twitter promise to keep 
disrupting in the wrong way. It was well worth it.

***************

You are  right on some big points. For example, that it is often important to be *disliked* by the right people. Or that 
when the design is bad, it might be better to  tear the entire thing down rather than prop it up.

(Actually, the Lean crowd seems to do such things with great gusto. The blog post by Thomas Hales I quoted in my 
previous mail says that "Lean 3 broke the Lean 2 libraries, and old libraries still haven’t been ported to Lean 3. After 
nearly 2 years, it doesn’t look like that will ever happen. Instead new libraries are being built at great cost.")

To state my differences with your position, I'd begin with the following statement: both mathematics and programming are 
social activities (like everything humans do), but are often done by particularly antisocial people.

The problem is that you seem to equate "social" with "political". And then in the next step you seem to equate 
"politics"---or at any rate good politics---with "subverting structures of oppression".

I guess that without this attitude, it would have been hard for you to carry high the banner of dependently typed 
programming when few other people believed, and take the risks that you took. So in this sense, it has served well not 
only you, but the entire community.

But if I might ask about your personal experience: would you say that after that "kicking against the pricks" (to quote 
King James Bible) period, when people started to rally under your banner after the good fight you fought, the 
development of Epigram, for example, was always best served by this set of views?

This is a genuine question. Epigram played an amazing rôle, inspiring Agda, Idris and Coq alike. I wish I had anything 
close to such a contribution on my CV. But in order to go beyond sometimes necessary subversion and inspiration, to 
build something that is not only based on brilliant ideas, but is actually used, with a growing community around it... 
maybe a different kind of politics is needed.

Let me quote again what Andreas Abel wrote in reply to Thomas Hales's excellent explanation of the good sides and the 
bad sides of Lean: "They say it takes 20 years to develop a proof assistant of some maturity (Coq, Isabelle, …). It is 
kind of reassuring for the competition that lean hasn’t reached that level in 5 years."

You don't me to tell you that, but one doesn't achieve such a lifespan in software without making sometimes painful 
compromises, without accommodating some "frozen accidents" and without the ability to cater to different communities 
with conflicting mindsets and needs.

[1/2 to be continued.... this email is getting too long]



> > Regarding Conor, as several persons actually privately expressed at
> > various degrees their perplexity on the point of his posts, it may be
> > good that he explains himself the actual message he's trying to
> > communicate. In any case, my feeling is that this is certainly not
> > against your own particular message but rather about more general
> > considerations.
> I've been reading this discussion with mixed feelings. I am particularly
> concerned that we take care and pay attention to the politics we are
> engaging in, even if we think we are being "scientists" and have somehow
> forgotten that we are human and exist in cultures and authority structures,
> of questionable merit, which we reinforce or disrupt by our actions.
>
> Our political motivations are inevitable: I would not criticise people for
> being political per se; rather I would criticise people for imagining they are
> not. And by acknowledging the political motivations for our design choices,
> we can begin to examine their opportunity costs, and the ways in which we
> have trapped ourselves, as well as the ways in which we are enabled.
> Beware of reasoning which goes "My tools solve my problems well, even
> though they solve your problems badly. Your problems are not important.".
> One must also ask "What does the fact that these people are beginning to
> like my system mean that I am doing wrong?".
>
> One can draw something of a parallel between proof assistants designed
> to attract mathematicians and dependently typed programming languages
> designed to attract functional programmers. Sometimes, conformity to other
> people's existing activity modes and power structures conditions us to
> leave more radical and powerful designs underexplored, prejudices and
> presumptions underquestioned. I'm similarly skeptical of attempts to ensure
> exchangeability of libraries between diverse systems: it restricts the
> diversification which is the point of having diverse systems. How are we to
> learn? But the radical road can be lonely: most established hegemonies
> don't especially feel in need of being saved, nor does it do anybody much
> good to imagine themselves a saviour. You get people to switch by having
> more fun than them in front of their kids.
>
> In this context, I view the plurality of our systems as a strength at this 
> point
> in the development of our discipline. It still feels like early days to me, 
> which
> is why it's great to be alive and working on this stuff. It's also in my 
> nature
> to be restless and discontented with the technology to hand: while much is
> possible, so much more is still painful, and we should not spare the time to 
> be
> pleased with ourselves. Rather, we should ask what we even think we'd like to
> keep about our systems and our cultures. I'm reassured by this discussion
> that the answer is not "nothing". I still can't help but hope that asking 
> which
> is the best proof assistant today will turn out to be like asking which is the
> best slide rule.
>
> Stay questioning
>
> Conor