Re: [sl4] prove your source code

From: Krekoski Ross (
Date: Wed Jul 16 2008 - 06:52:35 MDT

granted we want a model that can show this, but I havent a clue even
how to begin to approach it when we cant even start from static source


On Wed, Jul 16, 2008 at 8:46 PM, Krekoski Ross <> wrote:
> Yes but as I was saying, the code is not stable.
> Ross
> On Wed, Jul 16, 2008 at 8:15 PM, Wei Dai <> wrote:
>> 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