[gclist] Finalization, again
Sat, 06 Oct 2001 23:00:13 -0400
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
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
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.