The

I’m not going to talk much about it, though – instead I’m going to direct you to this extraordinary proof, written in verse, in the style of Dr. Seuss. It’s called Scooping the Loop Snooper, and it was written by Geoffrey K. Pullum, who you might also know from posts at the Language Log. Wow.

*unsolvability of the halting problem*is a well-known fundamental result which says that it’s impossible to write an algorithm that determines if an arbitrary program halts given some input. It also implies a lot of other things – including, for example, that there’s no general way to determine whether a particular variable in a program has a particular value at a point, and famously, that every consistent formal system powerful enough to do arithmetic in will have unprovable statements.I’m not going to talk much about it, though – instead I’m going to direct you to this extraordinary proof, written in verse, in the style of Dr. Seuss. It’s called Scooping the Loop Snooper, and it was written by Geoffrey K. Pullum, who you might also know from posts at the Language Log. Wow.