On Jan 28, 2008 7:41 PM, Matt Mahoney <[EMAIL PROTECTED]> wrote: > > It is easy to construct programs that you can prove halt or don't halt. > > There is no procedure to verify that a program is equivalent to a formal > specification (another program). Suppose there was. Then I can take any > program P and tell if it halts. I construct a specification S from P by > replacing the halting states with states that transition to themselves in an > infinite loop. I know that S does not halt. I ask if S and P are equivalent. > If they are, then P does not halt, otherwise it does.
Yes, it's what I was telling all along. > > If computer cannot be hacked, it won't be. > > If I turn off my computer, it can't be hacked. Otherwise there is no > guarantee. AGI is not a magic bullet. Exactly. That's why it can't hack provably correct programs. This race isn't symmetric. Let's stop at that (unless you have something new to say), everything was repeated at least three times. -- Vladimir Nesov mailto:[EMAIL PROTECTED] ----- This list is sponsored by AGIRI: http://www.agiri.org/email To unsubscribe or change your options, please go to: http://v2.listbox.com/member/?member_id=8660244&id_secret=90631134-afef0e
