Stream: coq-community devs & users

Topic: Coq vs. Lean comparison


view this post on Zulip Karl Palmskog (Nov 27 2021 at 17:18):

I'm starting to get sufficiently annoyed at "How is Coq different from Lean" questions, both online (e.g., https://twitter.com/MonniauxD/status/1463910928894894082) and by paper reviewers, that it might be time to just sit down and at least collect the sources for a comparison. Maybe a coq-lean-comparison coq-community repo makes sense?

What are the differences between Coq and Lean ?

- David Monniaux (@MonniauxD)

view this post on Zulip Karl Palmskog (Nov 27 2021 at 17:22):

maybe we can get actual type theorists to audit a comparison once there is enough material (i.e., shoot down the initial feeble slogans on canonicity and the like)...

view this post on Zulip Théo Zimmermann (Nov 28 2021 at 09:12):

We can expect this to be one of the questions that will be asked in the Proof Assistants Stack Exchange, so getting started on the answer could be worthwhile.

view this post on Zulip Karl Palmskog (Nov 28 2021 at 12:49):

in that case, a wiki page is probably better. But do Stack Exchanges allow essay-length answers?

view this post on Zulip Paolo Giarrusso (Nov 28 2021 at 13:38):

Pretty "long" answers are allowed, but a 10-page PDF wouldn't really fit. Multiple answers per responder are allowed tho, and can be useful for different aspects.

view this post on Zulip Karl Palmskog (Nov 28 2021 at 13:55):

OK, so we could "abuse" the system by answering "How is Coq different from Lean" by different people and explaining different aspects (foundations, tooling, ...), each with a long answer

view this post on Zulip Paolo Giarrusso (Nov 28 2021 at 14:06):

since self-answering is encouraged, I don’t think this is abuse — as long as you’re not gaming reputation by colluding everything goes.


Last updated: Feb 05 2023 at 14:02 UTC