Re: [sl4] prove your source code

From: Krekoski Ross (
Date: Wed Jul 16 2008 - 06:46:38 MDT

Yes but as I was saying, the code is not stable.


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