There is a distinction between "constructive" mathematics (AKA "intuitionistic") and "non-constructive" mathematics (AKA "classical").
In constructive mathematics, the only way to prove that something (e.g. a number) exists is to give an algorithm that constructs it.
We can do this in classical mathematics too (roughly speaking, it's a super-set of constructive mathematics); but we can also prove that something exists in another way: by disproving that it doesn't exist (i.e. a double negative). In other words, classical mathematics lets us use a proof of 'not(not(X))' as a proof of 'X'. There are some other ways to express this, which are essentially equivalent; e.g. the "law of the excluded middle" 'for all X, either X is true or not(X) is true'. These proof steps are not constructive, since knowing that not(X) is false doesn't tell us how to actually find/construct X. Likewise, the law of the excluded middle is like writing an if/then/else statement where both branches will arrive at the same result, but it doesn't tell us which of those branches to take.
We usually talk about proofs being constructive or non-constructive, rather than values (e.g. numbers). A constructivist shouldn't agree with a non-constructive proof, but they should agree with an alternative, constructive proof of the same result.
The interesting philosophical question being made here is: if a value's existence can only be proved non-constructively, should constructivists disbelieve in that value? In this case that value is the busy-beaver function: it can't be defined constructively, since no algorithm can decide the halting problem.
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.
In constructive mathematics, the only way to prove that something (e.g. a number) exists is to give an algorithm that constructs it.
We can do this in classical mathematics too (roughly speaking, it's a super-set of constructive mathematics); but we can also prove that something exists in another way: by disproving that it doesn't exist (i.e. a double negative). In other words, classical mathematics lets us use a proof of 'not(not(X))' as a proof of 'X'. There are some other ways to express this, which are essentially equivalent; e.g. the "law of the excluded middle" 'for all X, either X is true or not(X) is true'. These proof steps are not constructive, since knowing that not(X) is false doesn't tell us how to actually find/construct X. Likewise, the law of the excluded middle is like writing an if/then/else statement where both branches will arrive at the same result, but it doesn't tell us which of those branches to take.
We usually talk about proofs being constructive or non-constructive, rather than values (e.g. numbers). A constructivist shouldn't agree with a non-constructive proof, but they should agree with an alternative, constructive proof of the same result.
The interesting philosophical question being made here is: if a value's existence can only be proved non-constructively, should constructivists disbelieve in that value? In this case that value is the busy-beaver function: it can't be defined constructively, since no algorithm can decide the halting problem.