I interpret John Harrison as saying, among other things, that one can
always write complex decision procedures in a style in which they
output proofs. It seems to me that the real issue is one of constant
factors. A constant factor of 100 can be the difference between
feasible and infeasible. It seems very likely to me that in the four
color theorem an HOL tactic would run a factor of 100 or more slower
than a C program (probably more like a 1000). Of course to use a C
program in a foundational verifier one would have to verify C (as John
notes). Since the four color theorem is by now fairly old, it may be
feasible to solve it with a slow program. But other "black-box"
theorems may be more challenging, e.g., recent results on the
non-existence of certain quasi-groups. It seems to me that
cutting-edge black-box theorems will always be challenging for a
foundational prover unless it can verify and run C code or some
imperative equivalent.
I am not saying that these black-box theorems are important to the QED
effort. Rather, they seem like the primary place where computational
extensions, such as reflection, might pay off.
David