LCF-style provers like Isabelle/HOL and HOLlight are some of the most widely used, and oldest interactive theorem provers. If they consistently show smaller error rates than other systems, that is an interesting empirical observation. To give but one recent example: Amazon recently announced a vast 260000 lines of Isabelle/HOL-checked correctness proof of their new Nitro hypervisor for AWS EC2 Graviton5 instances.
LCF-style provers have a much smaller trusted computing base than Curry/Howard based provers like Coq, Agda and Lean.
One may wonder if there is a correlation between size of TCB and error rate in widely used provers?
LCF-style provers have a much smaller trusted computing base than Curry/Howard based provers like Coq, Agda and Lean.
One may wonder if there is a correlation between size of TCB and error rate in widely used provers?