The discussion in the comments has helped clarify your question for me. I believe that it is closely related to the following remark by Harvey Friedman:
I am convinced that trying to take consistency statements like Con(ZFC +
measurable cardinals) or Con(ZFC + rank into itself), Con(ZF + inaccessible
rank into itself), etc., and force them into smaller and smaller Turing
machines not halting, with demonstrable equivalence in an extremely weak
system, is an open ended project, in the practical sense, that will create a
virtually unlimited opportunity, in the practical sense, for a stream of
ever and ever deeper mathematical ideas. Ideas that could come from
unexpected sources, ideas that could have independent deep ramifications,
ideas that -- well who knows what to expect. The benchmark is completely
clear - how many quadruples? At the very least, deep ideas about set theory
and large cardinals, but probably much more diverse deep ideas about, well,
the unexpected. Any branch of mathematics whatsoever might prove useful, or
even crucial, here. Whereas, we don't think that "any branch of mathematics"
might be useful in logic problems, normally. This is different.
Other relevant postings from the FOM archives may be found here and here.
So Friedman's work, that Andres Caicedo alluded to in the comments, is probably the closest thing to what you want. I don't know of any other people who are working actively on this kind of project.
As a side remark, I believe that your intuition is correct that there is some kind of intrinsic "complexity" to the statement "ZFC is consistent," and roughly speaking it is because the totality of mathematical knowledge is a "complex" entity.
The first thing to notice is that if ZF is consistent, then it is
consistent with ZFC that what you call ProveLoop is actually decidable. The
reason is that if ZF is consistent, then by the incompleteness
theorem, it is consistent with ZFC that $\neg$Con(ZF), in which case everything is provable in
ZF, in which case every program is in ProveLoop.
So in the proof that ProveLoop is undecidable, one needs to make
an additional assumption about the reliability of the proofs in ZF to
avoid this issue with the incompleteness theorem.
Meanwhile, under such a consistency assumption, ProveLoop is indeed
equivalent to the halting problem.
Theorem. Assume Con(ZF). Then ProveLoop is Turing
equivalent to the Halting problem.
Proof. Under the Con(ZF) assumption, it follows that whenever ZF proves that a program doesn't halt, then it really doesn't halt, since if it did halt, then this fact would also be provable, contrary to consistency.
Clearly ProveLoop is c.e. and hence reducible to the
halting problem, as you pointed out. Conversely, let's reduce the
halting problem to ProveLoop. Given any program $p$, we want to
decide whether $p$ halts on a blank tape, using an oracle for
ProveLoop.
Define a computable function $f$, so that $f(q)$ is the program
such that, on trivial input, if $p$ halts on the blank tape, then
$f(q)$ jumps into an immediate infinite loop, and otherwise, while waiting for $p$ to halt, the program $f(q)$ halts just in case it finds a proof that $q$ does not halt.
By the recursion theorem, there is a program $r$ such that $r$ and
$f(r)$ compute the same function, and we can find this $r$
effectively. Furthermore, by using the $r$ from the proof of the recursion theorem, we may also assume that ZF proves that $r$ and $f(r)$ compute the same function. Notice that it can't ever be that $r$ halts on account of finding a proof that $r$ does not halt, by our assumption which ensures the accuracy of proofs of non-halting, and so definitely $r$ does not halt in any case. Meanwhile, if $p$ halts, then $r$ does not halt, but for a trivial reason that will be provable in ZF, namely, the fact that $p$ halted; and otherwise, when $p$ does not halt, then $r$ will run forever, but this fact will not be provable (for if it were provable, then $r$ would halt, contrary to consequence of our assumption that such proofs are reliable). So what we have is exactly a reduction of the halting problem to ProveLoop, as desired. QED
Best Answer
To my way of thinking, the two notions of undecidability are closely related, and the associated undecidability phenomenon and independence phenomenon, which are both pervasive in mathematics, are deeply inter-twined.
The reason is that every Turing undecidable set is saturated with logical undecidability. If we describe a certain undecidable property of finite graphs, say, then there will be infinitely many specific finite graphs for which it will be logically undecidable, even with respect to very strong theories such as ZFC+large cardinals, whether that finite graph has the property or not. And similarly with any undecidable set $A$ and consistent c.e. theory $T$. This is because if almost all instances of "$n\in A$?'' were settled by $T$, then we would have a decision procedure for $A$, namely, on input $n$, search for a proof from $T$ whether $n\in A$ or not (and hard-code the finitely many exceptions).
So every Turing undecidable property is accompanied by a huge assortment of logically undecidable statements, assertions about whether particular objects have the property or not, which are independent of whichever fixed consistent background theory you care to adopt.
So although the two undecidability phenomenon are distinct, I find them to be deeply connected.
Update. Let me clarify exactly how much we need to trust the theory for this argument to work.
Theorem. If $A$ is any computably enumerable computably undecidable set and $T$ is any consistent theory extending PA, then there are numerous instances of $n\notin A$ such that $T$ does not prove this. Consequently, if $T$ is $\Sigma_1$-sound, then these membership statements are independent of $T$.
Proof. Notice first that if $n\in A$, then PA and hence also $T$ will prove this. Therefore by consistency, $T$ is reliable in any proof of $n\notin A$. Consider the algorithm that on input $n$ undertakes the following: during the day, it enumerates $A$ and searches for whether $n$ appears; at night, it searches for a proof in $T$ that $n\notin A$. If all instances of nonmembership were provable, this would be a computable decision procedure for $A$, contrary to assumption. So there must be many nonmembers of $A$ such that this fact is not provable in $T$. If also $T$ is $\Sigma_1$-sound, then it follows that the statement $n\in A$ is independent of $T$. $\Box$