--- Vladimir Nesov <[EMAIL PROTECTED]> wrote: > On Jan 28, 2008 6:33 PM, Matt Mahoney <[EMAIL PROTECTED]> wrote: > > > > It is undecidable whether a program satisfies the requirements of a formal > > specification, which is the same as saying that it is undecidable whether > two > > programs are equivalent. The halting problem reduces to it. > > Yes it is, if it's an arbitrary program. But you can construct a > program that doesn't have this problem and also prove that it doesn't. > You can check if program satisfies specification if it's written in a > special way (for example, it's annotated with types that guarantee > required conditions).
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. > 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. -- Matt Mahoney, [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=90619751-b7cda9
