The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

On 1/2/20 6:00 PM, Kevin Buzzard wrote:

On Thu, 2 Jan 2020 at 21:55, Adam Chlipala <adamc AT csail.mit.edu> wrote:

I'm not sure I understand this point.  Ltac works well for most kinds of
tactic programming.  At least, I don't see how it could be held not to
meet the binary requirement of "a rich programming environment with
useful abstractions."

I am not a computer scientist and I don't have much experience with Coq,

but with Lean you only need to learn one language not two,

    It's not clear to me that reducing the number of languages is a
    clear win, when we often design new languages to better suit
    different use cases.

and as well as

writing tactics people have been writing things like linters, new commands

which tell you which namespace you're in, which namespaces are open,

what variables you have and so on, stuff which makes the end users life

a bit easier.

    At least in Coq, I feel like all of the above kinds of queries are
    obviated by the default display in proof mode.  I get the feeling
    "namespace" means something different and more subtle in Lean,
    though.  (And I've never seen the need for a "linter" in mechanized
    proof, especially for experienced users.)

In general, I think it's a mistake to compare proof assistants using
criteria associated with random varieties of open-source projects, since
typically open-source projects are much less involved in major
design-space innovations.  IMO, worrying about quality of library
ecosystems should mostly be avoided.

When mathematicians come looking at these systems, one of the first questions

they seem to ask is "how much mathematics is in there already?".

    I think today it makes a lot more sense for pure math vs. program
    verification to try to codify the existing shared knowledge base,
    since it's so much better-established.  One issue with program
    verification is that it brings in different kinds of scalability
    challenges, such that it no longer makes sense to think in terms of
    "which famous theorems are proved," but rather "which tools are
    available for new verifications."  Tactics can be just as important
    as theorems, and they very rarely correspond neatly with decision
    procedures.