Could the Halting Problem be "resolved" by escaping to a higher-level description of computation?

I've recently heard an interesting analogy which states that Turing's proof of the undecidability of the halting problem is very similar to Russell's barber paradox.

So I got to wonder: mathematicians did eventually manage to make set theory consistent by transitioning from Cantor's naive formulation of the field to a more complex system of axioms (ZFC set theory), making important exclusions (restrictions) and additions along the way.

So would it perhaps be possible to try and come up with an abstract description of general computation that is more powerful and more expressive than Turing machines, and with which one could obtain either an existential proof or maybe even an algorithm for solving the halting problem for an arbitrary Turing-machine?

Well, you can always consider a Turing machine equipped with an oracle for the ordinary Turing machine halting problem. That is, your new machine has a special tape, onto which it can write the description of an ordinary Turing machine and its input and ask if that machine halts on that input. In a single step, you get an answer, and you can use that to perform further computation. (It doesn't matter whether it's in a single step or not: it would be enough if it was guaranteed to be in some finite number of steps.)

However, there are two problems with this approach.

-
Turing machines equipped with such an oracle can't decide their own halting problem: Turing's proof of the undecidability of the ordinary halting problem can easily be modified to this new setting. In fact, there's an infinite hierarchy, known as the "Turing degrees", generated by giving the next level of the hierarchy an oracle for the halting problem of the previous one.

-
Nobody has ever suggested any way in which such an oracle could be physically implemented. It's all very well as a theoretical device but nobody has any clue how to build one.

Also, note that ZFC is, in a sense, weaker than naive set theory, not stronger. ZFC can't express Russell's paradox, whereas naive set theory can. As such, a better analogy would be to ask whether the halting problem is decidable for weaker models of computation than Turing machines. For example, the halting problem for deterministic finite automata (DFAs) is decidable, since DFAs are guaranteed to halt for every input.

StackExchange Computer Science Q#44763, answer score: 18