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?
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)...
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.
in that case, a wiki page is probably better. But do Stack Exchanges allow essay-length answers?
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.
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
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