4 ms·
How does Lean compare to Coq? And which one would be preferable for non-mathematicians trying to learn more about math? Which one would be better if you come fr
by elcapitan 5y ago
How does Lean compare to Coq? And which one would be preferable for non-mathematicians trying to learn more about math? Which one would be better if you come from a software background and want to do formal verification for parts of your programs?
- srl 5y agoThis is only a partial answer, but my understanding is that Lean is really not meant for software verification work. That's very much Coq's alley. I'm much less certain of this, but I think Lean is better for non-mathematicians trying to learn more about math --- provided, that is, that you're set on playing with a proof assistant. I'm not sure I'd recommend that.
- mbrodersen 5y agoNot true. Lean and Coq are very similar. However it is true that Coq has more of a history when it comes to verifying software (CompCert is written in Coq for example). And Lean is the state of the art when it comes to mathematics (mathlib).
- logicchains 5y agoThere's an excellent online book that introduces Coq and how to use it for verification of programs: https://softwarefoundations.cis.upenn.edu/ https://softwarefoundations.cis.upenn.edu/. There's also a more advanced book, http://adam.chlipala.net/cpdt/ http://adam.chlipala.net/cpdt/, that goes into more detail. In comparison, Lean has little teaching material for formal verification of programs.
- elcapitan 5y agoThanks, that's very helpful!
- logicchains 5y agoYou're welcome!