Re: Proof by construction, again (was Re: [sl4] prove your source code)

From: Tim Freeman (tim@fungible.com)
Date: Sat Jul 19 2008 - 13:29:16 MDT


--- On Sat, 7/19/08, Tim Freeman <tim@fungible.com> wrote:
> Entity A could prove to entity B that it has source code S by
> consenting to be replaced by a new entity A' that was constructed by a
> manufacturing process jointly monitored by A and B. During this
> process, both A and B observe that A' is constructed to run source
> code S. After A' is constructed, A shuts down and gives all of its
> resources to A'.

From: Matt Mahoney <matmahoney@yahoo.com>
>But A cannot know if S is its own source code. (I assume that S
>includes current state information needed to make a copy of
>itself). If it could know, then A could simulate itself (with infinite
>recursion, which is impossible).

The above proof technique also leads to the conclusion that backing up
my computer is impossible. My computer cannot possibly know all of
the bits it uses, since if it could, it could simulate itself, with
infinite recursion, which is impossible.

The gap there is that knowing the bits does not imply having the
capacity to run them. Simulating itself requires knowing what to
simulate, and also having the computational capacity to simulate.

Suppose my computer is configured to have 1GB of virtual memory. It
can't simulate a full version of itself, but it can simulate itself
with 750MB of virtual memory. The simulation overhead of 250MB of
memory might not be missed in everyday use, but it does stop the
infinite recursion after a fairly small number of levels, or maybe
after just one level depending on how brittle the definition of "my
computer" is. None of that stops me from backing up my computer.

Talk of "current state information" doesn't make a difference. At one
time there were patches that let Linux hibernate to disk. If I
successfully installed those, I could copy a machine-state to disk and
back that up, as it was before the start of the backup.

-- 
Tim Freeman               http://www.fungible.com           tim@fungible.com


This archive was generated by hypermail 2.1.5 : Wed Jul 17 2013 - 04:01:03 MDT