Here's a 40-minute video in which Tom Stuart gives a talk summarizing one of the chapters from him new book Understanding Computation, describing the halting state problem and how it relates to bugs, Turing machines, Turing completeness, computability, malware checking for various mobile app stores, and related subjects. The Halting State problem -- which relates to the impossibility of knowing what a program will do with all possible inputs -- is one of the most important and hardest-to-understand ideas in computer science, and Stuart does a *fantastic* job with it here. You don't need to be a master programmer or a computer science buff to get it, and even if you only absorb 50 percent of it, it's so engagingly presented, and so blazingly relevant to life in the 21st century, that you won't regret it.

At Scottish Ruby Conference 2013 I gave a talk called Impossible Programs, adapted from chapter 8 of Understanding Computation. It’s a talk about programs that are impossible to write in Ruby — it covers undecidability, the halting problem and Rice’s theorem, explained in plain English and illustrated with Ruby code. The slides are available

This sort of thing is really a great idea — many people writing programs are entirely self-taught and understand little of computational theory. Understanding things like the halting problem will prevent them from the equivalent of attempting to square the circle or create a perpetual motion machine.

Magic: The Gathering is a universal system?? (Sorry if this is explained later in the video. I haven’t gotten past that slide.)

A quick search found this link: http://boingboing.net/2012/09/12/magic-the-gathering.html

You write “The Halting State problem … relates to the impossibility of knowing what a program will do with all possible inputs…”

Not exactly. It’s very possible to know what SOME programs do with all possible inputs. Think of a program that always prints “42” and stops, for example.

The Halting Problem proves that’s it’s impossible to have an algorithm that can be given ANY program and ANY input and say what that arbitrary program would do.

just purchased the book on O’Reilly an looking forward to an excellent read! thanks for the heads up on the video, great intro to the subject

This talk is cliffs notes on Goedel, Escher, Bach by Douglas Hofstadter.

Additionally, this notion that one cannot write tests well is ever so close to entropy and prior probability, without really nailing it. Statisticians would be unsurprised at the basic punchline, which admits that unlikely events cannot be guaranteed not to happen. Yes, a test of a “hello world” program might fail in some extreme edge cases, but if those edge cases are extremely unlikely, then we can still use the tests with almost perfect success. It’s great to see determinism break down to stochasticism in strange loops! I just wish he’d nailed this a little harder on the head.

yes but OTOH the fundamental insight here is that it is ‘trivial’ to produce extremely short programs that can not answer seemingly simple questions, can not function correctly. it’s not like the complexity you get when planning to build a city or a supercollider, it like starts right when you pick up the hammer.

this–together with successful ‘coping stragtegies’–is definitely something that each programmer should understand. i found the talk extremely helpful and instructive.

I agree that this is a well-presented talk!

But I disagree with the other opinion expressed in the original post. The wonderful thing about the halting problem is that although it is a deep result that reveals something very interesting and fundamental about general purpose computation, it *isn’t* very difficult to understand. The argument is surprisingly simple.

(Also: there was one part of the “coping strategies” section at the end of the talk that I think is misleading. Tom implies that if you want to know whether some interesting property holds for a program you have written, you have to live with inexaustive tests, or some other kind of approximation to certainty: that you can’t ever prove it for sure. Not so. For a particular interesting true property of a particular program you wrote, it probably *is* possible to model that property and prove it formally for that program. The reasons for not doing so are pragmatic ones – it’s usually much more trouble than it is worth, and you may be as likely to make a mistake in the modelling or formalization of the proof as you are in writing the program.)