In a recent diary entry, Raph mentions:

"Given the obvious usefulness of code, it's tempting to put a virtual machine into the proof checker and proof object file format. A proof can include code when it also includes a proof that the code is correct. Such a proof will also imply that the code is safe, by the way. The checker will verify the proof of the code first, then assuming it passes, just run it. The output can be entered into the database of statements proved correct, just as if it had been spit out from an inference rule."

Sounds like proof-carrying code, although Raph's approach has sort of switched this around (perhaps this is a purely semantic point); his idea is possibly more adequately described as "code-carrying proofs". Raph, have you looked at PCC? Any thoughts?

For whatever it's worth, I had a big interest in PCC not too long ago, and I still believe it has merit, but it seems to be bogged down in the security research world. One of my more fanciful flights while at OpenCola involved PCC, mobile code, and capabilities (of course, I was mostly thinking all in E too, along with some Haskell at the time), which I thought would all go very well with each other. Indeed, PCC has been used in the field of mobile code more or less since it's first proof-of-concept. The farthest I got was just in some conversation with co-workers. I didn't have an opportunity to start an actual project around it.