Whats the difference between open proofs and proof-carrying code (PCC)?
Proof-Carrying Code (PCC) is a software mechanism that allows a host system to verify properties about an application via a formal proof that accompanies the application’s executable code. In both open proofs and PCC, a user/host system can verify that a particular program meets a particular claimed property by re-examining the accompanying proof. But there the similarity ends. If host/end-user wants to prove a different property than what the PCC provided, the PCC need not include enough information to do that easily. If the host/end-user wants to change the executable code (to fix, improve, or customize it), there’s no guarantee that’s easy; the user might not even get the source code! If the host/end-user wants to understand or improve on the underlying system used to develop the proofs, there’s no guarantee that the end-user will receive that system. Thus, they are really quite different.
