There is a point where these values become uncomputable, but they still exist (for some definition of exist).
I guess this is the crux of the issue for me and what I'm struggling with. This does not seem obvious to me.
I do lack a lot of knowledge about the concept of interpretation, so maybe that's where my issue is?
In logic, a model is a "set" of objects and all the true facts about those objects. For example, the integers and "1+1=2,1+2=3...". If a model deals with truth, then a "theory" is a mathematical structure that deals with provability. For example, the theory of groups contains an axiom "a+0=a" that applies to any a.
We say that a model "models" a theory when everything the theory proves is true in the model. The integers are a model of a group.
But, the integers mod 2 ({0,1}) are also a model of a group, but a very different one.
So, consider the statement "1+1≠0". The theory of groups isn't powerful enough to prove or disprove this proposition. It is a false statement in the integers, but a true statement of the mod2 integers. So there is a gap between what is true in a model, and what is provable in a theory.
(Look up both godel's completeness theorem and his incompleteness theorem for more insight into this relationship)
Back to turing machines, our most popular foundations of math is a theory named ZFC. With this theory we can prove many things, but there are also many things that can't be proven or disproven. ZFC lets us prove that "BB(500) is an integer greater than 5". But it doesn't let us prove that "BB(500)=174936...35" (pretend that's a concrete number). In fact, there probably is a model of ZFC where it is true that BB(500)=174936...35, and there is also probably a model of ZFC where BB(500)=284729...86.
Axioms define what is provable, but godel showed that there will always be more true things than there are provable things (if your theory is finite-ish). Most concrete questions about the BB function will never be provable.
As a simple example, we know that BB(1000) <= BB(1001) (since you can encode the longest running 1000-TM with an extra, unused state as a 1001-TM) even though we will never know either of those values.
The argument that it grows faster than any computable function is similar in that it proves things without knowing concrete numbers. (I'd have to look up the details of the proof to say more)
Assume f(x) is computable and grows faster than BB(x). We can create a computable g(x) where g(x) > BB(x) for all x, by setting g(x) = f(x) + C for some suitable constant.
Now we create a computer program that does the following. 1. Get the size of the input program and compute g(n). 2. Run the input program for g(n) steps. 3. If it stopped, return true. If it's still running, return false.
This solves the halting problem. Since a computer program can't solve the halting problem, this program can't exist. Everything except "compute g(n)" is straightforward, so there must be no such function g, and no such function f.