What does it mean to say $BB(7918)$ is not computable from ZFC? In a paper by Scott Aaronson, I read that Busy Beaver of 7918 can't be computed from ZFC. But $BB(7918)$ is a specific finite natural number, call it $k$. So, using $k$ applications of the successor function starting from $0$, we can define it. Granted, there is not enough space in the observable universe nor enough time until the heat death of the universe to define it, but it doesn't matter, it can be defined in principle. So, am I misunderstanding something? Please correct my misunderstanding if I am wrong.
 A: Converting my comment into an answer and elaborating: "computed" is sort of a misleading way to say it. The theorem is that ZFC doesn't decide the value of this busy beaver number; that is, there is no $n$ such that ZFC proves $BB(7918) = n$.
The problem is not even that $n$ is very big, just that it encodes a question ZFC can't answer. Here is a simpler example: consider the number which is either equal to $0$ if ZFC is inconsistent or $1$ if ZFC is consistent. Then the incompleteness theorem says exactly that ZFC doesn't decide the value of this number, despite the fact that by definition it is either $0$ or $1$!
"Number" is also sort of a misleading way to say it; you'll get very confused thinking about this if you don't distinguish carefully between a number and a description of a number. What I gave above is a description of a number, and it's a description that evaluates to a different number in different models of ZFC depending on whether they do or don't believe that ZFC is consistent.
$BB(7918)$, similarly, is a description of a number, and to say that ZFC doesn't decide its value is exactly to say that it will evaluate to different numbers in different models of ZFC (by the completeness theorem).
(I guess there might be an additional subtlety here about what it even means to compare the values of different numbers in different models of ZFC. But I think in this case we're okay.)
