alt Hacker News> But people have regularly asked why Isabelle dispenses with proof objects. The two questions are essentially the same, because proof objects are intrinsic to all the usual type theories. They are also completely unnecessary and a huge waste of space.
I believe proof by reflection relies on proof objects? Georges Gonthier's proof of the four-colour theorem crucially uses proof by reflection.
Proof by reflection is accomplished by running some arbitrary program during proof checking that has been proven to only return a "true" result if the goal is true. You can do the exact same thing in an LCF system, and in fact that's arguably what a complex LCF "tactic" amounts to in the first place. If anything, the viability of proof by reflection simply shows that the divide with LCF-like checkers is not really that large.