Less Wrong is a community blog devoted to refining the art of human rationality. Please visit our About page for more information.

Hyphen comments on Permitted Possibilities, & Locality - Less Wrong

11 Post author: Eliezer_Yudkowsky 03 December 2008 09:20PM

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

Comments (21)

Sort By: Old

You are viewing a single comment's thread.

Comment author: Hyphen 05 December 2008 10:28:44PM 5 points [-]

The halting problem's undecidability prevents you from writing a program that is guaranteed to prove whether other arbitrary programs halt or not. You can't write a halting-checker program and then feed it the source code to your AGI and have it say "this halts" or "this doesn't halt".

You can prove that some specific programs halt. If you're trying to prove it about a program that you are writing at the time, it can even be easy. I have written many programs that halt on all input sequences, and then proved this fact about them.

Here's a super-easy example: print "hello world" provably always halts.