How does being classical help with automation? I'm more familiar with ACL2, which seems to gain a lot more on the automation front from being first-order than from anything else (though it has sort of a weird take on the excluded middle).
That's a subtle and deep question. One example are nominal techniques. Consider Nominal Isabelle. It is known that nominal techniques are contructive. However, when adding nominal techniques to a classical logic, it is natural to express some of this using double negation, leading to only a small blowup in formula size. Existing proof automation can easily handle this blowuip. Doing the same in a simple minded constructive way, leads to a massive formula size increase, defeating (at the time) existing proof automation.
This was a while back, maybe the problem has been solved now, I have not followed this field. But as far as I'm aware, the 'hammering' approach to proof automation that has been working well with Isabelle/HOL has been successfully ported to Coq/Agda etc.
CertiKOS is verified in Coq, I don't see why you say it isn't fit to get work done.
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.
Re:Concrete Semantics
by logicchains on Friday January 17, 2020 @11:55PM
(#22082380)
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?
Re:Concrete Semantics
by logicchains on Sunday January 19, 2020 @05:44AM
(#22090664)
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.
There is an additional dimension which is strength of the logic at hand. The logics Coq, Lean et al are based on are more expressive in various dimensions. Whether that's relevant to your use case depends on what kind of maths you are trying to formalise. If it is higher category theory, it matters a great deal, for program verification it tends not to be important b/c most program verification can be done in rather weak logics.