The Coq mailing list

[Théo Zimmermann <theo.zimmi AT gmail.com>]

> I'd like to amend my previous comments.  This is not the first time
> I've had some fears about proof systems like Coq leaving software
> engineers behind for the loftier ambitions of mathematicians.  I also
> felt that when the HoTT people first gathered here years ago.  I'm
> very thankful when mathematicians make contributions to proof systems,
> but worry that they will use their abilities and influence to tune these
> sytems more to their own liking and less to mine, and others like me.

This seems like a fear that is expressed every once in a while on this
list. But rest assured that software verification as an application of
Coq is never going to be neglected by the development team. In fact,
given the importance that Coq is taking in this area, a lot of
incoming bug reports and feature requests (and most external funding)
come from people in the area of software verification. Thus, a lot of
engineering and research time is devoted to solve these specific
problems. For instance, Ltac was praised in this thread by people in
the area of software verification, and the upcoming Coq 8.11 version
will ship with Ltac2, which is an improved (and typed) version of
Ltac.

In fact, it is much easier to improve the situation for existing use
cases (e.g. software verification and constructive mathematics) than
for the less common use cases that Kevin mentioned. Indeed, we are
very much influenced by the feedback we receive (from existing users)
and what we know already. It is much harder to get feedback from
newcomers / outsiders. At this point, I should thank Kevin for taking
time to share his thoughts with us (and Bas for starting the thread,
and everyone else for taking part in this very interesting
discussion).

Something that is worth mentioning when comparing Coq to Lean is that
given the wide spectrum of the Coq user community, the Coq development
team does not have the same luxury allowing to redesign everything and
producing a new major version every once in a while, or throwing out
use cases (like HoTT when switching from Lean 2 to Lean 3). We have to
proceed with caution, improve most things incrementally, and be
careful when introducing new features because that will require
maintaining them for a long time. Lean, and other proof assistants
with smaller communities such as Agda, can move faster and break
things, and of course, this will lead some people to feel like Coq is
lagging behind...

Théo