[JadeNB]

> The halting problem makes it impossible to consistently answer the question "Will this instruction be executed ?"

In fact, Rice's theorem says that it's impossible more generally to answer any question about arbitrary code—so no work-arounds like "OK, I can't tell if a particular instruction is executed, but I can just test whether this program is 'safe'" (say, performs no I/O).

[chriswarbo]

Technically, Rice's theorem only applies to "non-trivial" questions, i.e. those which are true for some programs and false for others, which are properties of the function being computed.

Hence we can work around the theorem, by either turning the questions we care about into trivial questions, or by turning questions of the function into questions about the implementation.

For example, we might ask the question "Will program P fire the missiles?". If the answer is yes for some P and false for others, then we cannot answer it for arbitrary P.

We can work around it by weakening the question to become trivial, e.g. "Is program P capable of firing missiles?". If the language allows missiles to be fired, then the answer is trivially yes for all P; if not then the answer is trivially no.

Alternatively, we can change the question to one of implementation, e.g. "Does program P contain the <fire missiles> instruction?". Assuming that our programming language contains such an instruction, this is a non-trivial question. However, since it's a question about the implementation (does that instruction appear) rather than the function being computed (which may or may not fire missiles), Rice's theorem doesn't forbid us from answering it.

[JadeNB]

> Hence we can work around the theorem, by either turning the questions we care about into trivial questions, or by turning questions of the function into questions about the implementation.

You're quite right that my omission of 'non-trivial' makes the theorem as stated wrong; sorry!

I like your statement of the second work-around (elaborated below (https://news.ycombinator.com/item?id=11260034)), as (essentially) what type systems do, especially with the emphasis on why it must be over-conservative.

Although your statement of the first work-around is technically correct, I think that it is important to emphasise (as you clearly know, but others may not) how useless it is (on the program level): questions of this sort are necessarily about the language, not about the program.

[0x0]

> However, since it's a question about the implementation (does that instruction appear) rather than the function being computed (which may or may not fire missiles)

On common architectures where code is data is code, this sounds hard to detect as the program could build a buffer of commands that end up firing the missile, without any obvious "fire the missile" sequence present in the binary? For example, the program could inflict a stack overflow on itself.

[chriswarbo]

> the program could build a buffer of commands that end up firing the missile, without any obvious "fire the missile" sequence present in the binary

Absolutely, the work-arounds are just that; they don't answer the original question.

In the case of "Is program P capable of firing missiles?", this will be 'yes' for many programs which don't fire missiles, so it's an over-approximation of missile-firing.

In the case of "Does program P contain the <fire missiles> instruction?", this could, as you say, under-approximate missile firing.

If the language allows running data as code, then we can handle this in a conservative way, i.e. 'Could program P execute a <fire missiles> instruction?', which would be true if P contains '<fire missiles>', true if P contains 'eval' (since the evaluated code could fire the missiles), etc. and false otherwise. We can make our questions (AKA our type systems) arbitrarily clever, but they will only ever approximate the answers to questions forbidden by Rice's theorem. Usually it's best to make conservative approximations, i.e. turning "does XYZ happen?" into "could XYZ happen?", assuming that it could, and only answering 'no' if we can prove otherwise.

As far as cases like 'the program could inflict a stack overflow on itself', these would all be handled in our model of the language (equivalent to the list of conditions I wrote above which affected whether we answer true or false). Again, this should be conservative, so it's likely that for edge-cases like 'inflicting a stack overflow on itself', there might not be much we can say about the program's behaviour; in which case we'd get a lot of 'yes' answers to our 'could XYZ happen?' questions, simply because we can't rule those things out.

[9mit3t2m9h9a]

And the reason why you cannot check that the program performs no I/O is because you cannot check if the I/O instructions are behind an infinite loop or an impossible condition or not.

It is definitely easy to verify that a program has no references to I/O instructions. This will reject programs like «if(false) then write("Hello")», so it is not a violation of Rice theorem (functionally equivalent programs are not treated in the same way). But you don't need to accept everything that is actually benign, you just need to make it easy to write benign code that passes the check.