On Jan 29, 2008 12:35 AM, Matt Mahoney <[EMAIL PROTECTED]> wrote: > --- Vladimir Nesov <[EMAIL PROTECTED]> wrote: > > Exactly. That's why it can't hack provably correct programs. > > Which is useless because you can't write provably correct programs that aren't > extremely simple. *All* nontrivial properties of programs are undecidable. > http://en.wikipedia.org/wiki/Rice%27s_theorem > This is false. You can write nontrivial programs for which you can prove nontrivial properties. Rice's theorem tells that you cannot prove nontrivial properties for programs written in Turing-complete languages and given unbounded resources and handed to you by an adversary.
> And good luck translating human goals expressed in ambiguous and incomplete > natural language into provably correct formal specifications. > This is true. ----- 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=90871958-149830
