BB(k) for a specific k is just a number. Ao just write it to the output. Proofing correctness is different from „computing“ and not required here.

> BB(k) for a specific k is just a number.

That's not as obvious as you might think. The value of BB(800) is independent of ZFC. So it isn't "just a number" if you're working in ZFC.

Hmm... As ZFC specifically cannot identify that number as special (at least as relates to the Busy Beaver function), maybe it is quite specifically "just a number"!

Ah, so pointing out that the number itself, being an integer, is computable even though the function isn't. Makes sense.

Perhaps you need larger and larger sets of axioms as k increases.

This is fascinating to me, because Turing machines can in principle be manifested as physical objects. It feels like you shouldn’t need axioms if you have the thing sitting in front of you, but on the other hand how else are you supposed to prove something doesn’t halt?

Still, if you have two axiomatic systems that disagree, what does that mean? Surely you can just run the machine in question for a certain number of steps to determine which system is right.

Ah, the issue is that one system may be able to prove the correct answer but it remains independent for the other system.