The Coq mailing list

[Timothy Carstens <intoverflow AT gmail.com>]

I'm not Kevin, but it's a public thread, so -

My experience with Lean+Coq has been that they suffer from many of the same challenges, but in different ways

* Universes. Either you're gonna have explicit lifting (Lean) or you're gonna have a cumulative checker (Coq). One is tedious to use, the other is relatively complex under the hood.

* DLL Hell. Lean and Coq both have a hard time building a big collection of user-contributed libs, since minor changes to the engines break old code. I'm not a maintainer for either system but it seems like both engines rely on these really sensitive inference algorithms. Minor tweaks to these algo's just completely wrecks backwards compatibility for tactic-mode proofs.

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

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

* Performance. If you set out to write a high-perf pCIC checker, and you're an extremely experienced software engineer, you'll probably succeed. 3 years ago I'd say this was Lean's greatest strength, but in recent years Coq has gotten waaaaay faster, so maybe this isn't as relevant as it once was.

* Language server. Last I checked, both had an ad-hoc approach to this.

Coq has improved vastly in each of these areas in my ~7 years of working with it. There's still more work to be done, but not so-much that I'd advocate for completely starting over.

From the outside, it looks to me like Lean won't be "ready" until it has solved all of those issues to the team's satisfaction. Thus, every year or so they throw away their old code base and start from scratch, including how to organize things like the standard library (really fam, could we just do a good job with it and stop moving the chairs around??)

Anyway, that's my 2 cents ;)

Happy New Years! Wishing everyone deep insights and clever proofs,

-t

On Thu, Jan 2, 2020 at 9:36 AM Bas Spitters <b.a.w.spitters AT gmail.com> wrote:

Dear Kevin,

You claimed
"Lean is like Coq but better"
https://wwwf.imperial.ac.uk/~buzzard/one_off_lectures/msr.pdf

There was a bit of discussion among coq users about what this means.
Did you have any concrete suggestions on how lean is better, and how
Coq could be improved?

While I'm at it, let me announce this workshop next week to the coq-community:
https://www.andrew.cmu.edu/user/avigad/meetings/fomm2020/

Best regards,

Bas