The Coq mailing list

[Timothy Carstens <intoverflow AT gmail.com>]

> On Jan 2, 2020, at 2:54 PM, Adam Chlipala 
> <adamc AT csail.mit.edu>
>  wrote:
> 
> 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?

It’s an IMHO, not a proven fact :)

History of programming environments has tended towards specialization and 
abstraction; my comment is about trust that this will continue in all niches, 
including tactics systems for proof assistants.

On the evidence front, I don’t know of many credible studies on the HCI of 
proof assistants (though I think I recently saw an effort at this from UW? 
I’m sure someone’s got a link. I don’t know if they dug into this question 
tho)

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

I’m not worrying, just pointing out the current situation. I hope I didn’t 
convey a sense that I think this situation is permanent.

Haskell was in a similar place in the early 2000’s, and with the work of Don 
Stewart and others, the situation turned around almost overnight.

Don’t worry, that day will come for Coq and Lean.

All my best,
-t