| 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 think this is true. On the other hand, technological improvements might mean
that we only lag a few years behind the state of the art. Besides, it doesn't,
as David notes, seem very relevant to QED, which is largely concerned with
"textbook" mathematics (and as such is already way behind the state of the
art). In verification applications the problem is more serious, since here
"brute-force" proof techniques are pretty common.
John.