[gclist] Finalization, again

[David Chase]

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?  (I suppose there's papers I should read.)
I can think of several reasons it ought not be hard:

1) most code runs in polynomial time, all the time (or
   it would if it contained no bugs).  There are certain
   notable exceptions -- ML type inference is one.

2) most code (at least, code that I write) I know that
   it is going to run in polynomial time, and I know why.
   Assuming an adequate language for expressing what I
   already know....

3) assuming (at analysis time) I put the code in something
   like SSA form, find loops, find induction variables,
   it seems like a lot of basic stuff is going to fall out.

4) I think, if we had a slightly better type system for
   composing/creating data structures, we could better
   leverage code reuse.  For example -- the analysis for
   amortized time for splay trees is a pain, but once it
   is done, the formula applies to any splay tree.

5) Someone I once worked with long ago, Tim Winkler, had
   the idea that most of the power of higher-order
   programming was at the level of expression, and that
   in many cases all of it could be removed from a program
   before execution in some sort of a preprocessing
   step, and that this simplifying assumption might
   make many things much easier to figure out.  I
   don't know where that went.

The devil, as near as I can tell, is in the detail of
(possibly) circular data structures and concurrent
modification of shared data.  Sort-of-functional
programming, anyone?  That would be a hoot, if the
only code that we could really, truly, trust for
blind downloading was, except for the external
state changes, functional code.



David Chase
chase@naturalbridge.com
drchase@alumni.rice.edu
chase@world.std.com