Why not? That implies that an 8000 state Turing machine which eventually halts when started with a blank tape doesn't exist. If any of them do (and it's trivial to simulate one), then exactly such a program can exist.
Well, there can indeed exist a program that writes out the number BB(8000). (In the sense that it is consistent with ZFC that there is a program that writes out the number of steps of the smallest contradiction in ZFC.)
What I don't believe that there exist a program that is a proper counter-example, that is, its halting is undecidable in ZFC, and it halts. Exactly because what I wrote earlier.
I don't believe that there exist such a program.