Key points and Importance of Decidability

Question

A language is decidable If a TM recognises the language and goes into an Accept or Reject state. As a dev. I think this is important as it would mean we could determine if a program contains buffer overflows or deadlocks. Also, the following problems are Un-Decidable:

• Does a program ever access an uninitialized variable.
• Do two context free grammars describe the same langauge.
• Does it make a difference if parameters to a subroutine are passed by reference or by copy-result

In terms of Decidability what would you say are the key points to Decidability and why is Decidability important (particularly to a developer).

Note: Bullet points are fine in answers - I can look up the topics myself. I just want to know what are the main points.

Answer 1

Maybe this belongs in the cstheory exchange, but I'll have a go at it anyway.

The key point is: some problems are undecidable, i.e. not solvable by an algorithm, so they should be tackled by other methods. Among these problems are many "meta-problems" concerning computer languages, for instance the problem of detecting a virus.

Having determined that a problem is undecidable, there are several possible courses of action:

1. Some problems may be semi-decidable, i.e. there is a semi-algorithm that solves some cases, but loops forever on other cases. When implementing a semi-algorithm, put a timer on it and return no answer when the time runs out.
2. Solve only a few, hopefully crucial parts of the problem by simplifying it.
3. 2 + ask the user for input when the problem becomes too complex.
4. Use a heuristic that gets the correct answer most of the time.
5. Use a different language, perhaps a non-Turing complete one.

1 to 3 are popular for automated reasoning tools, including program verifiers. 4 is what virus scanners do. 5 is a good choice when allowing users to write scripts to automate a larger system; instead of giving them full JavaScript/Scheme/Lua/whatever, give them a restricted subset that does not allow unbounded recursion/loops.