In human mathematics black boxes are becoming more common. The four
color theorem is the best known example. Here we prove that if a
certain program terminates and prints t then the theorem is true. We
then run the program see that it prints t and believe the theorem.
The proof (the trace of the computation) is too long for humans to
check with confidence.
It seems that black-box theorems, such as the four color theorem,
would be a good test of the "LCF suffices" conjecture. Do you know if anyone
has tried to use a foundational verifier such as HOL to verify any such
black-box theorem?
David