In trying to understand the Halting Problem better, I am trying to come up with classes of provably non-terminating programs. 

For example, any program (including input) which leads to a finite-length infinite loop (with perfectly repeating state+tape) should be detectable. That leaves mostly induction/search problems like "get the first non-Goldbach even number above 4" as candidates. 

Clearly, some of these halt, and some can be proven non-halting (eg we know "find $n$ such that $n\cdot 0=5$ " and "find a proof that the Poincare Conjecture is false" would not halt). More generally, it seems every non-halting problem corresponds to a Diophantine equation which (provably or not) has no solutions. This leads to a seemingly fairly general algorithm to find many non-halting programs:

1. Convert Turing machine to corresponding Diophantine equation with one unknown
2. Feed the equation, along with First-Order Peano Arithmetic, to Prolog/Isabelle/your favorite proof assistant
3. Assert the existence of a solution
4. Derive 0=1

So, my questions: 

* Is there a more natural way to search for such contradictions using the formalism of Turing Machines (or some other more conventional model of computation), without converting to Diophantine equations?
* Are there *provably* non-terminating functions that can be found using some other algorithm, but not this one? What algorithm(s)? Would that require a "stronger" version of arithmetic?
* If there are such algorithms, is there any notion of a "biggest" class of provably non-halting programs, or would that somehow lead to solving the Halting Problem (or some other contradiction)?
* Are there any good references/keywords for this? I've searched for "provably non-terminating functions", but haven't come up with much

PS Feel free to fix/reformat anything, alert me to obvious theoretical mistakes, or let me know if this is a bad question.

EDIT: Some points to address responses so far:

* I know that it's "easy" to prove that a program halts--just run it until it does; the challenge is to prove that a program does not halt, which obviously isn't always possible.
* Re: D.W.♦, I know we can't enumerate all non-halting programs, and I know we can come up with many provable examples of non-terminating functions, I'm asking if there's a *most general* method of finding all non-halting programs that *can be* found/proven
* I am aware of the Curry-Howard correspondance that directly relates programs and mathematical proofs. However, because of the halting problem there can be no type for "non-terminating programs", and it's not immediately obvious how to type "provably non-terminating" either
* @chi's answer is exactly what I am looking for. To make sure I understand fully, let me restate my understanding of your enumeration of non-terminating programs, using the simplest possible axioms I can think of:

	1. Start with a basic definition of "strings" in pure First-Order Logic: 0,1,add0,add1,equality
	2. Define Turing machines using a rewrite relation on strings that captures the mechanics of a calculation step (ie, eval)
	3. Define big-step calculation $\rightarrow$ as the transitive closure of one-step eval
	4. Define a halting predicate as the existence of a fixed point
	5. For a given program $x$, prove $\forall y.x\rightarrow y\Rightarrow \exists z\ne y.y\rightarrow z$

So, would the above work? Is it equivalent to my Diophantine equation scheme? Is there a yet simpler version? Would more axioms (eg using naturals under Peano Arithmetic to encode the machines) be able to prove more non-terminating programs than this version, ie is there a more general method?