And you don't "throw away proofs" when using proof types. They are right there in the theory file if you want to check them again.
> Because it is only the proof calculi that have proof objects that seemingly need to put everything into the kernel.
I interpret that to mean that for some reason, having proof objects requires or at least encourages putting more logic in the kernel (which is apparently equivalent to having more axioms) and that results in a greater risk of having bugs in the proof checker itself.
As I understand their writing, ML is a language meant for developing proof assistants and this debate is specific to proof assistants written in ML, about the extent to which you use ML's type system as part of the kernel (proofs or theorems are types, at least partially), or write one yourself (proofs are just objects).
Even Rust has an unsound type system that allows arbitrary memory access in safe code, so you can't just assume your programming language has a sound type system.