Is there a variant of "there exists a program that prints BB(8000)" that doesn't rely on some sort of axiom of choice? Maybe the intuitionists have a more useful definition of computibility if it doesn't posit that such strange machines exist.
Why does it rely on the axiom of choice? It’s a consequence of the obvious fact that for every integer n, there exists a program that prints n. This doesn’t require choice.