[gclist] Finalization, again

[Nick Barnes]

At 2001-10-07 03:00:13+0000, David Chase writes:
> At 12:09 PM 10/5/2001 +0100, Nick Barnes wrote:
> >Proof-carrying code, Necula et al, addresses exactly this sort of
> >point.  You need to know that some code (e.g. a downloaded applet) has
> >certain properties (runs in a given amount of time, doesn't perform
> >"illegal" accesses, doesn't raise exceptions).  So you require that
> >the code should come with a proof of these properties.  You can check
> >the proof in a small finite time.  Generating such a proof is very
> >much harder(!).
> 
> How hard is it?

To prove safety properties of downloaded machine code?  Potentially
very hard indeed!  This is what I was comparing to the cost of
checking a proof, in the above paragraph.  Sorry that it wasn't clear.
My point is that the code producer can generate a proof fairly
cheaply, and attach it to the code, and that the code recipients can
then automatically and cheaply validate the proof.  If the proof
validator is accurate, the code recipients then know facts about the
code which they could not otherwise reasonably discover.

For the code producer, it's not nearly so hard to generate a proof,
for many reasons including ones which you go on to identify.

In the finalizer case, this can also apply when the producer is the
mutator and the recipient is the GC (or the producer is the programmer
and the recipient is the language runtime, or ...).

> (I suppose there's papers I should read.)

Google gave me <http://www.cs.berkeley.edu/~necula/pcc.html>, which
seems like a good place to start.  It's quite a while since I read up
on this.

Nick B