Yes, I agree with you that a correct JVM can guarantee memory safety at the bytecode level, but what I meant to express was that many JVMs have had bugs that caused them to fail to do so, for essentially social reasons which I expect to cause problems with other PCC systems as well.

Maybe you're right, and those problems are not inevitable; for example, if you could reduce the proofs to a tiny MetaMath-like kernel that wouldn't need constant "maintenance". As you say, that could move the compiler's optimizer out of the TCB — at least for the security properties Fil-C is enforcing, though the optimizer could still cause code to compute the wrong answers.

That seems like something people would want if they were already living in a world where the state of computer security was much better than it is now.