> 'halting' could have been substitued with 'somewhere in the program variable x gets set to 5' and you could still construct a program in which it would be imp

> 'halting' could have been substitued with 'somewhere in the program variable x gets set to 5' and you could still construct a program in which it would be impossible to prove whether or not x gets set to 5. Rice's theorem extends the Halting Problem in a very general way. The idea is that for any program 'foo', we can invent a new program 'bar; foo;' which will only execute 'foo' once 'bar' has halted. Since the halting problem is undecidable in general, and 'bar' can be any program, it's undecidable whether such a program will eventually execute 'foo'. Any property that depends on whether or not 'foo' gets executed is hence undecidable. However: there are many properties which don't depend on whether 'foo' will eventually be executed. For example 'does this program take more than 1000 steps to halt?' is decidable, since we can just run the program for up to 1000 steps to see if it halts or not. More subtley, we can check things about the syntax, e.g. 'does this program contain a call to the "LaunchTheMissiles" function?'. That's easy to decide by just looking at all of the tokens in the code. Of course, this doesn't tell us whether such a call would ever be reached, e.g. it would flag a program like if (false) { LaunchTheMissiles(); } else { ImplementWorldPeace(); } This program would never launch the missiles, but it's often enough to spot potential issues, even if our errors are overly-conservative. Such false-positives can be really annoying when we try to retro-fit such checks on to languages which weren't designed for them; e.g. trying to spot pointer errors in C code or potential nulls in Java code. In contrast, designing them into the language from the start can be really useful. For example, that's what type systems do. For example, consider the following code: String foo() { if (true) { return "hello"; } else { return 123; } } This is perfectly correct, since it claims to return a String and it will return a String. However, every type checker in the world will reject this program due to the mere presence of the 'return 123' branch. This is quite a common pattern in programming language research: problems which are undecidable in most languages can be made trivial by designing the language with that problem in mind. In this case their 'while' example in C is very illustrative: there's not enough information in the code to know which (if any) of the loop iterations rely on the previous ones having been executed first. The fact that it could rely on execution order means we can't safely parallelise it. In contrast, a call like 'map(something, myList)' implies that each element's processing is independent (hence why MapReduce is popular for parallelism!).