I 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.