I think what you are describing is program verification, not proof-carrying code. In proof-carrying code, of course, the proposition you are proving may not

I think what you are describing is program verification, not proof-carrying code. In proof-carrying code, of course, the proposition you are proving may not be associated with the source code as an invariant. But if it isn't, why isn't it? It makes no sense to have one language for the invariant and another for the program. For example, one use of PCC is to prove propositions about a bit of machine code, such as a packet filter. When you create an environment that can state propositions about machine code, you have created a typed assembler, whether you like it or not. Most leaders in the Netflix challenge are (at) CS departments because CS departments are full of smart programmers.