Here is the debate as I understand it: (And forgive me if I mix language from multiple domains please.)
The Intuitionists argue that all mathematics can be stated operationally, and as such, for all intents and purposes, all mathematical symbols other than the glyphs we use to name the natural numbers, are nothing more than names for functions (sets of operations).
However, the intuitionist (‘recursive’) solution causes a problem in that the excluded middle is impermissible – but without it, much of mathematics because much more difficult, and harder to prove. So with that constraint on the excluded middle, the higher truth requirement of computational and constructivist, intuitionist logic has been deemed not useful for departmental mathematicians.
So under the ZFC+AC and ‘spontaneous platonic imaginary’ creation of sets, we obtain the ability to do mathematics that include both double negation and the excluded middle.
This ‘trick’ separates Pure math in one discipline and Scientific math, Computational mathematics, and philosophical realism into different discipline, each with different standards of truth. In fact, technically speaking, mathematics is absent truth (correspondence) and relies entirely on proof. ie: there are no true statements in pure mathematics.
IF ANYONE KNOWS —» It does not appear that Brouwer or any of his followers understood why their method failed and the set method succeeded. But even if they failed, I am trying to figure out if the Formalists understood their ‘hack’ and why it worked.
And lastly, if anyone at all understood how Intuitionist, constructivist, and computational logic could be improved to solve the problem of retaining correspondence (truth) while also retaining the excluded middle (even if it was burdensome).
Someone smarter than I am has got to have addressed this problem already although for the life of me I can’t find anyone who has.