paulfchristiano comments on What can you do with an Unfriendly AI? - Less Wrong

16 Post author: paulfchristiano 20 December 2010 08:28PM

You are viewing a comment permalink. View the original post to see all comments and the full post content.

Comments (127)

You are viewing a single comment's thread. Show more comments above.

Comment author: paulfchristiano 21 December 2010 07:32:34PM 2 points [-]

That is completely not what Godel's incompleteness theorem says. It may say that there are programs which are secure but not provably secure, but I don't care at all about that, because programs humans use are designed in a principled way and are not in fact designed to have their security be undecidable.

The difficulty of engineering more complex software which is provably secure increases quite rapidly, but no fundamentally new difficulties arise. In fact, the filters I describe in this article are quite simple for some problems; the one necessary for the proof of the Riemann hypothesis in fact already exists in a provably secure implementation.