I'm confused then because the paper linked in the OP states:
> The true source of uncomputeable functions is not the axiom if choice (which is valid intuitionistically) but the law of the excluded middle and indirect proof [emphasis original]
It is choice in constructible mathematics: something “totally different” from “zf” choice. Existence means “can construct”, essentially. There are “less” things in constructible mathematics than in zf.
This is a rough explanation.
> The true source of uncomputeable functions is not the axiom if choice (which is valid intuitionistically) but the law of the excluded middle and indirect proof [emphasis original]