Q1: Yes (except that the certificates you get may have size polylogarithmic in $n$, not just logarithmic, and you need to apply the argument to both HALTS-IN-N and its complement, as pointed out by Andreas).
Q2: Well, NP = EXP contradicts all kinds of conjectures from complexity theory: it makes the polynomial hierarchy collapse to NP = coNP, it makes NP = PSPACE, and PSPACE = EXP, all of which are assumed to be false. On the other hand, it also implies P ≠ NP. We cannot rule out NP = EXP with the present state of knowledge (nor the even stronger collapse ZPP = EXP), but the time hierarchy theorem implies that $\mathrm P\ne\mathrm{EXP}$ and $\mathrm{NP}\ne\mathrm{NEXP}\cap\mathrm{coNEXP}$. Existence of succinct certificates also shows up in other similar situations: for example, if EXP has polynomial-size Boolean circuits, then membership in any EXP language has succinct certificates verifiable in randomized polynomial time (that is, EXP = MA).
Vis-à-vis the last but one paragraph of your question, note that an exhaustive deterministic search for a short certificate takes time exponential in the size of the certificate, so you don’t save here anything in terms of deterministic running time.
I don’t follow the last paragraph. EXP = NP implies $\mathrm{DTIME}(2^{t(n)})\subseteq\mathrm{NTIME}\bigl(t(n)^{O(1)}\bigr)$ for every time-constructible function $t(n)$ of at least polynomial growth, if that’s what you mean, but this does not lead to a contradiction.
EDIT: It may be worth mentioning that there is nothing particularly revolting about the idea that the existence of an exponentially long computation can be proved using a polynomial amount of data. In fact, Babai, Fortnow, and Lund have shown that NEXP = MIP, which means that two (computationally unlimited) agents presenting polynomial-size evidence who cannot communicate with each other can reliably convince a randomized polynomial-time verifier that such an exponentially long halting computation (even nondeterministic) exists. (Here, polynomial and exponential is measured in terms of the length of the input, which is logarithmic in the $n$ from the original question.)
EDIT 2: Yes, the running times for primitive recursive functions (or predicates) are enormous. More precisely, a function is primitive recursive if and only if it is computable in time $A(k,n)$ for some constant $k$, where $A$ is the Ackermann function. Plugging an extra exponential or logarithm in this characterization makes no difference. In view of the latter fact, whether NP = EXP or not has not much to do with the argument: we know unconditionally that the version of HALTS-IN-N where $n$ is given in unary is in P.
Every r.e. language is polynomial-time reducible to the halting problem. Since there are computable languages (indeed, in $\Delta^E_3$) having the maximum possible circuit complexity for every length $n$ (which is asymptotically $2^n/n$), the halting problem also has exponential circuit complexity. The exact complexity will depend on the particular representation of algorithms in the definition of the halting problem, and specifically, on the complexity of the reduction function which hardwires an input string into a fixed algorithm. In the most obvious representations, this function blows up the input length only linearly and can be made computable by linear-size circuits, hence we get $2^{\Theta(n)}$ as the circuit complexity of the halting problem. If the halting problem is formulated directly for algorithms accepting an input, the reduction function increases the input length by an additive constant and has essentially constant complexity, so the circuit complexity of the halting problem is $\Theta(2^n/n)$ in such a formulation.
Best Answer
Here is one proposal.
A set of natural numbers is computably enumerable if it can be enumerated by a Turing machine program, that is, if the set is the range of a Turing computable function. Two such sets are said to be Turing equivalent, if each of them can be computed from an oracle relative to the other, and the resulting collection of c.e. Turing degrees is an extremely rich and intensely studied hierarchy.
Since every Turing machine program can be viewed as enumerating some c.e. set, we can naturally classify the complexity of the programs by the complexity of these c.e. sets that they enumerate, as points in the Turing degrees.
It was the famous Post's problem that asked whether indeed there were any c.e. degrees other than the decidable sets and the halting problem, but it was found that there is indeed a very rich hierarchy of intermediate c.e. degrees.