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