I think the question you are asking - about how can we trust a formal proof - is a very important question. I have spent considerable effort developing software to specifically address this question. You touch on various things I have concentrated on.
It is true that various systems prominent in the formalisation of mathematics - including the HOL systems (HOL4, ProofPower HOL, HOL Light), Isabelle and Coq - are built according to the "LCF style", which means that all deduction must go via a relatively small kernel of trusted source code (implementing the primitive inference rules). It is also true that this greatly reduces the risks of producing unsound proofs on these systems. It would not be an exaggeration to say that almost everyone working in formal proof is happy with this situation. Indeed, probably most (but not those working on the above systems) feel that resorting to the LCF style is overkill and an unnecessary drain on user execution time and on development effort.
There are 3 main problems with this status quo:
The LCF-style kernel is not as purely implemented as may be expected. Some systems have back doors to creating "proved theorems", such as importing the statements (but not the proofs) of previously proved results from disk, and trust that the user will not abuse this. Also, to reduce execution time, various derivable inference rules are implemented as primitives, multiplying up the size of the trusted source code. Also, the kernels typically incorporate large amounts of supporting code (e.g. for organising theories) and are not particularly clearly implemented, and so are difficult to review. It should be noted that HOL Light does not suffer from any of these problems.
The trusted source code in LCF-style systems is NOT limited to the LCF-style kernel. Like in all systems, it at least also includes the pretty printer, since, in practice, the user will only view results displayed via the pretty printer. However, each system has problems with its pretty printer that allows misleading information to be displayed to the user (e.g. by using irregular variables names, or names that are overloaded). I have found many ways of appearing to prove "false" in these systems! Also, depending on how the system is used, the parser is arguably also a trusted component.
The importance of the human process of checking that the intended result has in fact been proved (I call this "proof auditing") is generally greatly underestimated, and in practice often not even carried out at all. As you rightly point out, the axioms and definitions used in a formal proof need to be carefully checked, as well as the statement of the theorem itself. I have known subtle mistakes in definitions to render real proofs on real projects completely invalid.
So the concept of checking one system using another is not only philosophically reassuring, but also of pressing need. As you say, what is needed is the ability to port proof objects between systems (the so called "de Bruijn criterion"). Strictly speaking, the de Bruijn criterion is as you state your requirement - the ability to capture a proof as an object (e.g. a text file) - rather than the LCF style (but let's not get too philosophical about the equivalence of these approaches). Anyway, there are some practical issues here:
The "dumb program" that you refer to needs to be surprisingly sophisticated, otherwise it loses much of its purpose. If it is just an LCF-style kernel, the data it outputs will be too slow to review for large projects. As you say, it needs to be human-friendly - a decent pretty printer is a practical necessity. Also, to make proof exporting (see next item) work in practice, it needs to work at least at a slightly higher level than the kernel, and so some supporting theory is required to be built. So yes, a dumb program is required, which should be as easy to understand as possible, but it is more challenging to build than a few lines of code.
Capturing proof objects in a suitably efficient way is a non-trivial exercise. The work that others mention above successfully ports things like the base system of HOL Light, but falls over when porting something as extensive as Hale's HOL Light proof of the Jordan Curve Theorem.
Some sort of neat and trivial correspondence of equivalent theory between systems is useful. This is better than importing language statements as huge expressions, in terms of some highly-complex embedding of one notation inside another, which would either greatly increase the complexity of the checking system or make its human usage difficult.
Anyway, to cut a long story short, I have my own open source "dumb system", called HOL Zero. The idea is that it's a proof checker for other HOL systems. It has a watertight kernel, a robust printer and the source code aims to be as clear and well-commented as possible. It needs OCaml (a dialect of ML) and a Unix-like operating system. You can download it from here:
http://www.proof-technologies.com/holzero.html
I've also implemented proof porting that works on large proofs. It's about 15 times faster than other efforts. I've successfully ported Hale's HOL Light proof of the Jordan Curve Theorem to an old version of HOL Zero. I've also successfully ported Harrison's proof of the consistency of the HOL Light kernel. I need to update it sometime to work with the latest HOL Zero, and to port proofs from other HOL systems. Note that the proof porting aspect of HOL Zero is not yet available from the website.
All of this is based on a standard HOL API (not yet published, and still being tweaked). This API should hopefully enable interchange between any two conformant HOL systems, not just to HOL Zero as a target.