Re: [sl4] prove your source code

From: Wei Dai (weidai@weidai.com)
Date: Wed Jul 16 2008 - 06:15:37 MDT


Lee Corbin wrote:
> Naturally, they may have each other's source code at hand,
> and be able to study it at leisure. Doubtless they can even
> make some general prognostications. But I'm sure that by
> "know" you mean more than that.

Actually, the difficulty I had in mind was the seeming impossibility of
*proving* one's source code to another. Sure, one SI can just send her
source code to another, but how does the other SI know that it's not just
some source code that she wants him to think she's running?

It seems that if it *were* possible to prove one's source code to another,
interesting things besides superrationality, like for example self-enforcing
contracts, would be possible. (One simply modifies one's source code to
guarantee attempts to fulfill the contract terms and then prove the new
source code to the counterparties.)

>> I suspect that two machines of similar complexity and capacity
>> would run into a parallel concern.
>
>Seems clear to me too.

But the two SIs don't have to emulate each other perfectly. Assuming the
above problem is solved, they just have to prove to each other that the
source code they are running implements superrationality (or whatever). It
is a difficult problem to prove anything about an arbitrary program, but it
should be possible to construct a program in a way that makes the proof
easy. This is a known technique that goes under the name of "proof-carrying
code".
 



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