This is a good explanation. I just have one quibble: the school of constructivism that Andrej follows is not the only one; there is a Russian school that accepts Markov's principle, which is essentially the logical counterpart of the idea that there is a fact of the matter whether a deterministic Turing computation terminates. I don't know if constructivists from the Russian school allow BB to be definable, but the argument for it to be undefined is trickier on this account.

https://en.wikipedia.org/wiki/Markov%27s_principle