The idea is to minimize the trusted computing base---a compiler and runtime system for a high level language is a big and complicated system, so it is very hard to get it right, but a proof checker can be small so it is easier to be confident that it is correct. (This idea is also known as the "de Bruijn criterion").