On Mar-24, Dan Sugalski wrote: > At 12:36 PM +1100 3/24/04, [EMAIL PROTECTED] wrote: > >On 24/03/2004, at 6:38 AM, Dan Sugalski wrote: > > > >This is a question without a simple answer, but does Parrot provide > >an infrastructure so that it would be possible to have > >proof-carrying[1] Parrot bytecode? > > In the general sense, no. The presence of eval and the dynamic nature > of the languages we're looking at pretty much shoots down most of the > provable bytecode work. Unfortunately.
? I'm not sure if I understand why. (Though I should warn that I did not read the referenced paper; my concept of PCC comes from reading a single CMU paper on it a couple of years ago.) My understanding of PCC is that it freely allows any arbitrarily complex code to be run, as long as you provide a machine-interpretable (and valid) proof of its safety along with it. Clearly, eval'ing arbitrary strings cannot be proved to be safe, so no such proof can be provided (or if it is, it will discovered to be invalid.) But that just means that you have to avoid unprovable constructs in your PCC-boxed code. Eval'ing a specific string *might* be provably safe, which means that we should have a way for an external (untrusted) compiler to not only produce bytecode, but also proofs of the safety of that bytecode. We'd also need, of course, the trusted PCC-equipped bytecode loader to verify the proof before executing the bytecode. (And we'd need that anyway to load in and prove the initial bytecode anyway.) This would largely eliminate one of the main advantages of PCC, namely that the expensive construction of a proof need not be paid at runtime, only the relatively cheap proof verification. But if it is only used for small, easily proven eval's, then it could still make sense. The fun bit would be allowing the eval'ed code's proof to reference aspects of the main program's proof. But perhaps the PCC people have that worked out already? Let me pause a second to tighten the bungee cord attached to my desk -- all this handwaving, and I'm starting to lift off a little. The next step into crazy land could be allowing the proofs to express detailed properties of strings, such that they could prove that a particular string could not possibly compile down to unsafe bytecode. This would only be useful for very restricted languages, of course, and I'd rather floss my brain with diamond-encrusted piano wire than attempt to implement such a thing, but I think it still serves as a proof of concept that Parrot and PCC aren't totally at odds. Back to reality. I understand that many of Parrot's features would be difficult to prove, but I'm not sure it's fundamentally any more difficult than most OO languages. (I assume PCC allows you to punt on proofs to some degree by inserting explicit checks for unprovable properties, since then the guarded code can make use of those properties to prove its own safety.)
