I love that article but that does not state what you are claiming it does. What that states is that there exists a k (whose upper bound is 8000) whose solution is independent of ZFC. That does not mean it can't be computed.

In the very comment section of that blog post someone brings this issue up, and Scott himself says:

"Yes, fine, you’re right, there’s not a single “boundary between the knowable and the knowable.” What there is, is more like a concentric series of boundaries, with signs warning you that as you proceed outward you need to take on bolder and bolder axioms (which might be large-cardinal axioms and might be something else). What’s significant about going beyond ZFC is just that, by that point, you’ve clearly passed the first of those boundaries."

Suppose BB(8000) could be computed: 1) Compute BB(8000). 2) Run the program specified in the article until it either halts or it runs for BB(8000)+1 steps. 3) We then know if the program ever halts, and then have a proof within ZFC whether or not ZFC is sound.

No, what you will have is a proof that ZFC is sound but that proof will not be within ZFC. That proof will rely on additional axioms that are extensions to ZFC.

Well, OK, I suppose you could add something like 'BB(8000) is 6,' but once you go beyond ZFC, you're going beyond anything required for computation as we know it.

No this is also wrong. You would not be able to add an axiom like 'BB(8000) is 6' or just any arbitrary value without introducing an inconsistency. The reason for the independence of BB(8000) from ZFC is precisely because there is some non-standard model of arithmetic for which a Turing Machine halts in that non-standard model but does not halt in the standard model.

The only axioms you could introduce to ZFC that would not introduce an inconsistency would be one that eliminates that non-standard model of arithmetic without also eliminating the standard model of arithmetic.

https://en.wikipedia.org/wiki/Non-standard_model_of_arithmet...

None of this requires going beyond any kind of notion of computation and any value that is computed for one such extension would necessarily have to be the same value among all consistent extensions of ZFC. It's not like you could have one extension of ZFC where BB(8000) is X and another extension where BB(8000) is Y without one of those extensions being inconsistent.

There are plenty of extensions to ZFC that add new axioms for the sake of exploring niche mathematical ideas. ZFC is nice in that it's easily motivated and can serve as a well understood foundation whose proofs can be stated without reference to additional hypotheses. It also satisfies an unbelievably broad set of mathematics, but mathematicians studying set theory often extend ZFC with additional axioms such as large cardinal axioms, Neumann/Bernays/Godel (NBG) set theory is another common extension, Kelley Morse (KM) set theory. The latter two extensions are even able to prove the consistency of ZFC. As I referenced in Scott's quote, BB(8000) is almost certainly computable by adopting one of the large cardinal axioms.