7 ms·
I know. There have been a lot of impressive verification work in Coq. Huawei is using Coq to do OS verification. Having less automation to hand, in comparison w
by Cladode 7y ago
I know. There have been a lot of impressive verification work in Coq. Huawei is using Coq to do OS verification. Having less automation to hand, in comparison with Isabelle/HOL makes this a bit harder.
- logicchains 7y agoCoq has less built-in automation, but with Ltac it's possible to achieve impressive levels of automation through explicitly-crafted decision procedures, as demonstrated in Chlipala's CPDT and many of his papers.
- Cladode 7y agoYes, Coq has a tactics language. So does Isabelle. What I have in mind are primarily "Hammers", i.e. hooking in fully automatic theorem prover (e.g. MizAR for Mizar, Sledgehammer for Isabelle/HOL, HOL(y)Hammer for HOL Light and HOL4). As far as I'm aware, CoqHammer for Coq is work-in-progress and does not yet provide the level of automation that you get from Sledgehammer in Isabelle/HOL for years. But admittedly, it's been 4-5 years since I last used Coq. At the time, two core issues were the following: - Existing automatic theorem provers often produced non-constructive proofs. - Existing automatic theorem provers are mostly for FOL, so the gap to the much more powerful logics of Curry-Howard based provers is bigger than with weaker systems. Have both problems been solved comprehensively as of January 2020?
- logicchains 7y agoThey have not been solved. My point was that automation via Coq's tactic language can serve as a decent substitute for "push-button" automation like Hammers, at least if one's continually working in the same domain and so can build up a library of tactics.