@JoelDavidHamkins Ah, good to know; I'm not a proper set theorist, and I didn't look too closely into the precise statement. (I think I read that part at some point, but somehow conflated it in my head with $(\mathbb Z_p,+)$ not being orderable without dependent choice.) In any case, I mainly wanted to raise the idea that even though the full structure of a non-standard model is full of uncomputable dragons, there can still exist substructures that we can look at and manipulate explicitly.

True, I suppose it depends on your reference point for "many": I'd consider a dozen to be plenty enough, given how quickly the function grows. I remain optimistic about provability for "small" machines in principle, since the known-"hard" machines are all just gnarly statements in number theory, which we usually presume not to be too powerful in proof-theoretic terms. (Still, there are constructive systems which can prove infinitely many $\operatorname{BB}$ values: it's just that they're all either uncomputable or inconsistent!)

@GeoffreyIrving To make what Z. A. K. says more explicit, when we say that $\operatorname{BB}(n)\leq N$, we say that "for all $n$-state 2-symbol machines $M$, either $M$ halts in $\leq N$ steps, or $M$ doesn't halt at any step". Depending on the system, there are many particular pairs $(n,N)$ for which constructive logic can prove $\operatorname{BB}(n)\leq N$. But (assuming consistency) constructive logic cannot prove that "for all $n$, there exists an $N$ such that $\operatorname{BB}(n)\leq N$", since this requires LEM.

This link is dead: the paper's title is "On the representation of an integer in two different bases", and a live version can be found at uwaterloo.ca/pure-mathematics/sites/default/files/uploads/….