[Cryptography] Is it mathematically provably impossible to construct a mechanism to test for back doors in programs?

[Judson Lester]

On Wed, Jun 4, 2014 at 10:46 AM, Phillip Hallam-Baker
<phill at hallambaker.com> wrote:
> The way I generated proofs for the ZEUS data acquisition system was to
> design a very very high level language that was specific to a task and
> then generate the code and the proof together from the specification.
>
> What makes the system work is that these are not specifications in a
> generic language, they are specifications in a language for writing
> FSRs or Parsers or a routing harness on a parallel processor.

Sincerely curious: How do you demonstrate that the proof and the code
are both accurate representations of the specification? I'm thinking
back to a subverted GCC that was able to protect itself by modifying
programs as they were built. In other words, how do we know that the
proof of the specification applies to the proof of the code?

Judson