The article says "if the usual axioms of set theory are consistent, we can never use them to determine the value of BB(7910)." But why does this imply that BB(7910) is uncomputable? Perhaps another axiomatic system could compute its value?
I realise you're talking about formal systems specifically (which corresponds to a some theorem-checking TM implementing that system) but when you allow any system of axioms (e.g. one with the value of BB(7910) of axioms) you basically ask whether any TM can compute that number (including one that already 'knows' it).
Of course another axiomatic system could. If you could tell us such an axiomatic system for which you can prove that it can determine the value of BB(7910) and have strong arguments why it is probably consistent (by Gödel one will not be able to prove this property if it is able to express basic arithmetic) mathematicians would love to get to know it, since they really have no idea how such a system might look like.
And it's easy to go one level up, I.e that system plus it's own consistency.
These systems will be stronger than ZFC, and will prove the machine in question halts.
Of course, the lowest unknowable from ZFC BB number is probably around BB(15), so likely none of those systems get that high, but they do probably give us more than just ZFC does.
See also http://www.scottaaronson.com/blog/?p=697 for some limitations on this.
Also, there are large cardinal axioms which imply the consistency of ZFC and are believed to be consistent, but I'm not so familiar with them. I think mathematicians would consider those axioms as "what such a system would look like".
You might look at Believing The Axioms (http://cs.umd.edu/~gasarch/BLOGPAPERS/belaxioms1.pdf, but it's two parts) which studies set theorists who are investigating new axioms for set theory, especially large cardinal axioms, iirc. Honestly, that work is a ways beyond what I can understand, but it's clear that it's an active area of research.
You might also read about Hugh Woodin has a very developed program arguing for axioms which would imply the negation of the Continuum Hypothesis.
(This doesn't necessarily apply to this specific question, but in general, research into axiomatic foundations of math is ongoing).
You can get more powerful, it's just unlikely anything we can build will get that high.