I am answering one of your two questions, regarding the halting
First, the undecidability of the halting problem does not state that
you cannot decide whether a given TM does not halt. It states that
there is no general algorithm that can decide that for all TM.
This is a statement about our models of what constitute
computation. But, according to Turing-Church thesis, that is all we
have to express compuation.
Regarding the relevance, it is based on artificially constructed
Turing Machines. But then, all TM are pretty artificial and
constructed only to assert some facts about computation. Whether some
TM are more relevant than others in practice is pretty much as
important a question as the sex of angels, or the number of them that
can stand on a needle head.
The undecidability of the halting problem tells us that there are
general questions that cannot be solved by a general technique
applicable to all cases. What I mean by general question is a question
depending on some parameters, where the answer is to be found for some
values of the parameters.
Recall that the purpose of much of our mathematics is to find general
techniques to solve a family of problems. A typical example is the
resolution of equations. The undecidability of the halting problem
tells us that this is not always possible.
For example, it can be used to show that there is no general technique
to decide whether a context-free grammar is ambiguous.
However, you question is a valid one. It may be that a problem is
undecidable because you just made it a bit too general. Possibly, by
restricting it a bit, you can make it decidable for useful and still
large enough subfamily.
I do not have a spectacular example in mind, but I am sure there must
I recall one true case of a program analysis problem that was
proved NP-complete (unless it was undecidable, I do not remember
well). Against all advice, a PhD student decided to tackle it anyway.
He was actually able to show that some restrictions on the problem,
that did not matter much in practice, turned it into a very tractable
problem, thus enabling the use of various program analysis and