The relationship between large cardinals and program termination
This isn't really an answer, but it's way way too long for a comment. I just want to offer some commentary on the linked answer. Re: your actual questions, you might find this paper interesting.
I think that Neel's$^*$ comment is somewhat misleading.
Let's start from the basic side of things: how do large cardinals imply facts about arithmetic? (Via Godelization, facts about program behavior are "really" facts about arithmetic.) The simplest answer is via consistency claims. The statement "ZFC is consistent" is a $\Pi^0_1$ sentence (look up the arithmetic hierarchy if you're not already familiar with it). It is also implied (over ZFC) by the existence of a weakly inaccessible cardinal; this is because ZFC proves the statement "If $\alpha$ is weakly inaccessible, then $L_\alpha\models$ ZFC." So this is an example of a fact about arithmetic which is implied by a large cardinal statement.
This can be directly turned into a statement about program termination, as follows. For a given computably axiomatizable theory $T$ (such as ZFC), we can write a program $\pi_T$ which halts iff $T$ is inconsistent - basically, $\pi_T$ just searches for a proof of a contradiction from $T$, and halts iff it finds one.
As an aside: the task of finding reasonably small programs which "represent" certain properties of a given theory, or at least have meaningful properties which can't be proved in a given theory, is an interesting one. See e.g. this work by Aaronson and Yedidia on a short program which runs forever, but which ZFC can't prove runs forever.
Essentially, the following is a basic fact about computability and provability:
The consistency of a given computably axiomatizable theory $T$ is equivalent to the non-termination of a program associated to $T$, and consistency statements often follow from large cardinals.
So that's a sense in which large cardinals can lead to statements about the behavior of programs. It's even better than that: the program $\pi_T$ associated to $T$ is optimal, in the sense that a reasonable theory (much much less than ZFC - even less than PA!) proves that $\pi_T$ terminates iff $T$ is inconsistent. In particular, to each large cardinal axiom A we can associate a program $\sigma_A$ such that $\sigma_A$ terminates iff ZFC+A is inconsistent. So:
The consistency with ZFC of a given large cardinal axiom is equivalent to the non-termination of a certain program.
So this connects the consistency of large cardinals with the non-termination of programs.
But that's not what Neel said! He said that large cardinals were equivalent to statements about program termination.
Now on the face of it, this is outright false: statements about program termination are arithmetic statements, and these can't depend on the actual truth of large cardinal axioms. Precisely, if A is (what would generally be recognized as) a large cardinal axiom, then ZFC does not prove "$\varphi$ is equivalent to A" - or even "$\varphi$ implies A" for any arithmetic sentence $\varphi$ unless ZFC actually disproves A.
This may sound mysterious, but there's actually much less to it than meets the eye. Fix a large cardinal axiom A = "there is a cardinal $\kappa$ such that [stuff]." The [stuff] will always imply that such a $\kappa$ gives a model of ZFC, that is, that $L_\kappa\models$ ZFC (this is a sociological claim about what constitutes a "large cardinal" - the term "large cardinal" is not a precise one).
OK, so suppose ZFC doesn't disprove A. Then by Godel's completeness theorem, ZFC + A has a model $M$. Now let $\kappa$ be the least ordinal in $M$ such that either $M\models$[stuff]$(\kappa)$ or for some $\alpha\in Ord^M$, $\kappa\in L_\alpha^M$ and $L_\alpha^M\models$[stuff]$(\kappa)$. (This isn't necessarily the actual least witness to A - it could be smaller.) By the note above, we have $L_\kappa^M\models$ ZFC, but by definition of $\kappa$ we also have $L_\kappa^M\not\models$ A. However, the set of natural numbers didn't change between $M$ and $L_\kappa^M$ (since all we did was "cut (the $L$ of) $M$ off" at some infinite level), so $L_\kappa^M$ satisfies all the same arithmetic facts as $M$ itself - in particular, the truth value of $\varphi$ didn't change. So we've shown:
If A is a large cardinal axiom and $\varphi$ is an arithmetic sentence consistent (over ZFC) with A, then $\varphi$ doesn't prove A.
And the case when $\varphi$ isn't consistent (over ZFC) with A is of course trivial, since then $\varphi$ can't be equivalent (over ZFC) with A unless A is inconsistent.
So in what sense was Neel's claim correct?
I think he was making a point about the semantics of programming languages. This is not a subject I know much about, so I may be wrong here, but my understanding is as follows:
The idea here is to create an actual mathematical structure associated to a given programming language. My understanding is that often, if not usually, this structure is a category with various nice properties and possibly additional structure. Incidentally, the precise details of the structure can be subtle - see e.g. this discussion of whether the "categorical" semantics for Haskell actually is a category. (I am totally unqualified to comment on this specific issue, by the way. If you're interested you might ask a question here about it.)
The point now is that the following can, and apparently does, occur:
There is a semantics $\mathcal{S}$ for a programming language FOO, such that the non-termination of certain programs in FOO are equivalent to the existence of certain corresponding large cardinal axioms, appropriately re-interpreted into the relevant framework, in the structure $\mathcal{S}$.
That is, the construction of $\mathcal{S}$ from FOO is somehow canonical, and we're not speaking of the non-termination claim as implying the genuine existence of a large cardinal, but rather as implying a fact about the internal structure of the object $\mathcal{S}$.
Note the phrase "appropriately re-interpreted." A large cardinal axiom stated in the language of set theory doesn't immediately make sense in the context of, say, category theory. Instead, we need to look for an appropriate equivalent. A neat example of this is the equivalence, due to Blass, of the existence of a measurable cardinal and the existence of an exact functor $F$ from Sets to Sets which isn't naturally equivalent to the identity. Now, if we're given some "appropriate" category $\mathcal{C}$, it perhaps makes sense to say "$\mathcal{C}$ thinks there is a measurable cardinal" iff the statement "there is an exact functor $\mathcal{C}\rightarrow\mathcal{C}$ not equivalent to the identity" is true.
So I suspect that this is what Neel means when he says that claims about termination are equivalent to set-theoretic claims: that when we look at the canonical semantics for a given programming language, termination facts are reflected by internal set-theoretic properties of that structure.
$^*$I'm not sure what the etiquette is regarding names; I've used first name, but I'm happy to use full name or professional title or etc. if that's the better standard.