Karl Palmskog (Nov 27 2021 at 17:18): 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) 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)...
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.
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?
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.
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
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: Jun 03 2023 at 17:29 UTC