The Coq mailing list

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

On 1/2/20 2:41 PM, Timothy Carstens wrote:
> * Tactic mode. Arguably this should be a rich programming environment 
> with useful abstractions. Right now you can get that if you're willing 
> to write a Coq plugin, but that's kinda heavy-handed, and it's 
> certainly a highly-coupled (hard to maintain) way to go. Lean has a 
> goal of offering a richer environment for tactics. IMHO everyone will 
> eventually need to go in this direction.

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."

How common is it for people outside the core Lean development team to 
write their own nontrivial tactics?  In other words, is there evidence 
that Lean's tactic style is attracting more satisfied users?

> * Few user libs, and even fewer that actually build on each other. 
> This is a bad sign for both environments - healthy software ecosystems 
> have towering stacks of libs and tools with meaningful dependencies.

I think what we really see here is that mechanized-proof engineering is 
such a young field, mostly confined to basic research, that we don't 
know enough about which reusable abstractions to build, so we certainly 
don't know how to connect those abstractions in nice ecosystems.  At the 
same time, we shouldn't confuse the current state with the projected 
state of a production-quality ecosystem once most basic-research 
questions are worked out.

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.