Hacker News Reader

Comment by Cladode | Hacker News Reader

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.

View on HN

Coq 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.

Yes, 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?

They 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.

Reply on news.ycombinator.com