alt Hacker NewsI do not get why not needing proof objects is desirable. It seems good to have a defined way to store proofs that has a very tight spec and can thus have competing implementations, like in https://arena.lean-lang.org/. The LCF approach couples the proof format to the module system of a programming language.
Occasionally, inspecting that proof term is useful to see what happened in a proof.
Then again, I also like dependent types.
You can use reflection in dependently-typed proof systems to avoid storing proof objects for expensive computations and replace them with a proof of a general algorithm instead (much like in the LCF approach: the general algorithm proof is the equivalent of a compiler checking that the module system use in a LCF tactic is sound).