I have to admit that I know very little about formalized proofs, but the article seems to put some reasoning behind this distinction, specifically this statement:

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