Are there any proofs the undecidability of the halting problem that does not depend on self-referencing or diagonalization ? This is a question related to this one. Putting it again in a much simpler form after a lot of discussion there, that it felt like a totally different question.

The classical proof of the undecidability of the halting problem depends on demonstrating a contradiction when trying to apply a hypothetical HALT decider to itself. I think that this is just denoting the impossibility of having a HALT decider that decides whether itself will halt or not, but doesn't give any information beyond that about the decidability of halting of any other cases.

So the question is


  Is there a proof that the halting problem is undecidable that doesn't depend on showing that HALT can not decide itself, nor depends on the diagonalization argument ?


Small edit: I will commit to the original phrasing of the question, which is asking for a proof that doesn't depend on diagonlization at all (rather than a just requiring it to not depend on diagonalization that depends on HALT).
Yes, there are such proofs in computability theory (a.k.a. recursion theory).

You can first show that the halting problem (the set $0'$) can be used to compute a set $G\subseteq\mathbb N$ that is 1-generic meaning that in a sense each $\Sigma^0_1$ fact about $G$ is decided by a finite prefix of $G$. Then it is easy to prove that such a set $G$ cannot be computable (i.e., decidable). 

We could replace 1-generic here by 1-random, i.e., Martin-Löf random, for the same effect. This uses the Jockusch-Soare Low Basis Theorem. 

(Warning: one might consider just showing that $0&#39;$ computes Chaitin's $\Omega$, which is 1-random, but here we have to be careful about whether the proof that $\Omega$ is 1-random relies on the halting problem being undecidable! Therefore it's safer to just use the Low Basis Theorem).