Automated proving that a program doesn't halt If you are a computer and you are given a program $P$ (with no input parameter) that doesn't halt, how would you try proving it doesn't halt ?  (here proving means convincing ourselves that it is true)
I guess most people would say to translate the statement &quot; $P$ doesn't halt &quot; into an arithmetic sentence $\forall n, S(n) \ne 0$ (where $S(n+1) = P(S(n))$ is the $n$-th state of the program) and enumerate the theorems of PA until it proves the sentence.  Or is there a more elegant way ?
Ie. how would you try (and success in) solving the halting problem, except in a few pathological cases  ?
Then I'd like to get some intuition on how to visualize (and solve) those pathological cases arising from undecidable problems (in PA). Is there a way to solve them (except in a $\scriptstyle\text{fewer}$ pathological cases) using a new routine enumerating the theorems of a meta-theory (which one) ?
Finally, is it hard to write the concrete code of all this, will it be readable and useful for teaching and for the intuition ?

Concretely I'm asking if this is the algorithm I'm supposed to think to, in that case can I find the concrete code of it somewhere :

Input : a program $P$ with no arguments. Let $ S(n+1) = P(S(n))$ be its sequence of states.
Compute $S(n),n=1,2,\ldots$. If for some $n ,S(n)=0$ then output &quot;$P$ halts&quot;.
In the same time enumerate the parenthesized and annotated sentences of PA, where the annotation indicates which inference rules to apply, thus it is trivial to check if a given sentence is a valid theorem of PA and if it proves $\forall n, S(n+1) = P(S(n)) \land S(n) \ne 0$, in that case output &quot;$P$ doesn't halt&quot;.
The other cases ($P$ doesn't halt but PA doesn't prove it) are said pathological.
In contradiction with Gurkenglas' answer, there actually is a community of scientists who work on proving non-termination of programs in various language and formalisms.

An obvious approach would be to check for looping non-termination: for a given program $w$, pick an input $x$ and check to see if the same state is reached twice with the same data.

Non-looping non-termination is obviously more complex, but has been studied, e.g. in Emmes &amp; al Proving Non-Looping Non-Termination Automatically or Endrullis &amp; al Proving Looping and Non-Looping Termination by Finite Automata.