Yes, you can prove termination of non-trivial programs; Halting just says you cannot do this for all possible programs. In terms of proving termination for practical programs you would want to write though, it's feasible to do but requires more effort for harder algorithms.

For example, many functions can be defined using primitive recursion which is very easy to check: http://en.wikipedia.org/wiki/Primitive_recursive_function

Primitive recursion really says "when defining f, you can only call f recursively if the arguments you call f with are simpler each time". This ensures that eventually some kind of base case is met and the function terminations. Examples of these kinds of function are list operations like reverse, insert, remove, filter, append, map, drop etc. These terminate on an empty list and the recursive call makes the list smaller each time.

For more general recursion, you can prove termination by providing a "termination measure". This is some value of some kind that you prove gets smaller on each recursive call. An example of this is a binary search, where the reducing termination measure is the distance between the two search markers. Termination proofs usually involving thinking about how you yourself know that the program terminates and then justifying this logically.

There are plenty of systems that support automated and assisted termination proofs. Have a browse on google for decades worth of work into this problem:
http://www.google.com/search?num=100&hl=en&q=termination+proof+automatic&btnG=Search&meta=

regurgitates what the above poster said in first sentence. ha ha ha taking a course in computation and intractability huh? man, now that was a fun class.

Now is it possible to say

a) it does halt.
b) it doesn't halt.
c) I can't tell if it will or not.
d) I can't tell if it will or not and here's the reason.

it would very handy for a post compiler check.

Predicate maths helped me tidy up my code immensely. I found it really useful, finally I could say WHY I coded things in particular ways I had discovered by trial and error.

Quote:Original post by ROBERTREAD1
Now is it possible to say

a) it does halt.
b) it doesn't halt.
c) I can't tell if it will or not.
d) I can't tell if it will or not and here's the reason.

it would very handy for a post compiler check.

Predicate maths helped me tidy up my code immensely. I found it really useful, finally I could say WHY I coded things in particular ways I had discovered by trial and error.

Yes and I can even give you the pseudo-code:

function Halt?  return can't tell

That satifies your description of it, so without any other guarantees about what kind of halting it detects it would be useless.

Quote:Original post by ROBERTREAD1
Now is it possible to say

a) it does halt.
b) it doesn't halt.
c) I can't tell if it will or not.
d) I can't tell if it will or not and here's the reason.

it would very handy for a post compiler check.

Predicate maths helped me tidy up my code immensely. I found it really useful, finally I could say WHY I coded things in particular ways I had discovered by trial and error.

The Halting problem is undecidable which means there does not exist a yes/no procedure that can tell you what will happen always. Your compiler could have:

a) it halts (e.g. it doesn't use recursion for trivially halts; it is defined by primitive recursion; it has a valid terminating measure)
b) it doesn't halt (e.g. I can prove the input to the recursive call always grows)
c) I do not know if it halts (it might be have, say, a terminating measure or a proof that it loops forever but the system just isn't smart enough to find it)

An example of c from http://en.wikipedia.org/wiki/Halting_Problem (worth a read, it's well written) is:

function findTwinPrimeAbove(int N)
int p = N
loop
if p is prime and p + 2 is prime then
return
else
p = p + 1

If you can find if this halts, you have an answer to the unsolved twin prime conjecture (i.e. a really hard long standing math problem). The conjecture could be true or it could be false, so until we prove/disprove it we won't know if this function halts or not.

There are compilers/system that exist today that can check for termination. See here for an annual competition on termination checking:
http://www.lri.fr/~marche/termination-competition/2006/

speaking of that twin prime thingy oh i bet the OP just can't wait till they cover goedel's incompleteness theorem ha ha ha. oh, that was fun too lol. oh the things that lurk in a computation class...

Is Gödel's incompleteness theory and the halting problem related?

Maybe Gödel's unprovable axioms are equivalent to a set of assumed functions that always halt?

The First Incompleteness Theorem and the Halting Problem (also the Church Turing Belief/Argument, whose truth or not places constraints on the universe because of the first two theorems) are all related. I have seen a proof of Godels Theorem in terms of the Halting theorem.

As well, both the incompleteness theorem and halting hinge on a method quite similar to Russell's Paradox to express their thesis and so will have similar structures. But no, they are not equivalent I do not think. I think Godel's might be more general.

I have a question that I hope someone may answer. I know of a language - Charity - that does not suffer from the Halting Problem, all programs on it terminate. That is, it is not turing complete. What are the consequences of this on the scope and applicability or strength of the language?