It's possible to provably construct a program that will halt. That is the whole point of loop invariants. Similarly it is possible to provably construct a "secure" program up to physical limitations. However in both cases it requires that the semantics of the programming environment are known to the programmer. Even without a malicious adversary there are gotchas at every level from hardware bugs, compiler bugs, programming errors, incorrect configuration, and who knows what else that impair the programmer's ability to understand the actual semantics of the programming environment. When you add to that the potential for maliciously clever modifications such as the one in the Thompson paper along with the undeniably large benefit to any number of parties that might wish to compromise same, the only rational conclusion is that no computing system deserves to be trusted in itself.

I don't trust other levels of the alleged chain of trust either. For example I consider it an absolute certainty that every competent globally active intelligence agency in the world has assets inside Facebook and Google, and most likely others. The cost and difficulty of inserting or recruiting an asset is so low and the potential benefits are so high that it's certain to have happened and in fact already has[1].

By the way while my ex-NSA buddy didn't elaborate on what he meant by attacking the implementation, but I'm pretty sure that includes subverting an implementer.

Edit: I don't think we really substantially disagree, the above is meant to be elaboration not rebuttal.

[1] https://www.washingtonpost.com/world/national-security/nsa-i...