[efaref]

But do you even trust the compiler they use?

Computers you don't totally control are inherently untrustworthy: http://cm.bell-labs.com/who/ken/trust.html

For most things it doesn't matter enough, but for deciding who gets to run the country, I think we need a higher standard.

[bmm6o]

I know everyone likes to cite that paper whenever they can, but it's not really relevant here. In this hypothetical, they give you the source but they compile it to binary. They do not provide you with the compiler or its source. The compiler can be malicious, but there's no need to hide its maliciousness - they don't even prove that the software running is in any way derived from the source they've given you! It would be a giant leap forward to have to design against KT-level shenanigans. The whole process can currently be subverted with CS 101-level jiggery pokery.

[SixSigma]

So why not also demand the object code. Then you can mistrust the hardware instead.