The Coq mailing list

[Conor McBride <conor AT strictlypositive.org>]

I'll accept Hugo's injunction to comment at greater length.

I also apologise for being the wrong kind of disruptive.

> On 11 Jan 2020, at 17:35, Hugo Herbelin 
> <Hugo.Herbelin AT inria.fr>
>  wrote:
> 
> Dear Tadeusz,

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

> 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