Post #1870928

For a long time I believed that one of the advantages of dependent type theory for applications to SW/HW verification was that it naturally incorporates proof by reflection (since the kernel type checker can do nontrivial computations). In particular, this comes in handy when dealing with decision procedures. Even when they can produce a proof (e.g. SAT solvers producing resolution proofs), the proof term is usually too large for this approach to scale to real problems. And there are many cases where the ability to produce a proof is elusive, e.g. the AIG-based simplifications required to implement an industrially relevant bitvector SMT solver. However, in practice, I don't think the situation is really any different than it is for HOL-based systems. Kernel computation in Lean is too slow to actually run the "verified verifier" in the kernel, so it is compiled by the code generator and an extra axiom is added to trust the execution of the result. This might be a bit more viable with Rocq (because it has array computation in the kernel whereas Lean does not), but I suspect that in practice you'd run into similar limitations. In the end, this isn't really any different than extracting programs from a monadic subset of HOL, compiling those programs, and then trusting the result. If you want to go to the next step and have truly end-to-end verified reflection, then it seems that projects like Milawa and CakeML are further ahead than anything based on DTT, and the proofs involved appear to be simpler than even the "basic" metatheory for a realistic variant of CiC.