I think you're right on the money bringing Turing into this.

I don't have a real, formal horse in this race, but the way that I have things arranged in my mind is that these are all disagreements on the notion two things in logical foundations: the need to consider time/resources and the conception of logical systems as closed or open.

Brouwer and Hilbert accept that time is a factor, but handle it in different implicit ways. Hilbert differentiates between finite (time accessible) and infinite (not finite) and then makes a plea that this divide doesn't much matter. His Program sought to prove it and then Turing and Godel and the like shattered that dream. Brouwer philosophically treated proof as communication and thus Intuitionism handles time and resource naturally (though not explicitly like a Kripke model).

Brouwer was forced by this choice to leave his mathematical foundations open ended as well. At any given level of effort there is a finite set of things we can prove/talk about/know and the rest must be left unknown, but likewise at any point in time we can incrementally increase our knowledge. Intuitionism is complex in order to handle that openness.

Bringing Turing in makes openness and expense/time immediately obvious. Turing machines are a model for an open world of knowledge: once you have a partial halting oracle G I can build a new program which your oracle fails on. Godel took it to the next level: your own formal system cannot prove its own consistency, but using it I can create a larger universe where it can be proven consistent.

In each case, the result arises from wanting a formal closure of your foundation and both use self-reference to create a (co-)inductive means of incrementally enlarging your system forever.

So I think Brouwer beats them to the punch in a certain way by taking that continuous finitary expansion as foundational itself.

Free choice can't be modeled formally by "Turing machines" because we possess a means for writing them all down. On the other hand, if I give you the trace of a Turing machine you have no (finite) means to predict it so "Turing machine traces" do provide the largeness you need. I don't really know how to handle the fact that someone might want to form a bijection between the two. To me it makes me think immediately of information hiding behind an abstract interface: even though you could eventually know an implementation of the interface, you spend most of your time working ignorant to it and often have more power for doing so.

I'm definitely no expert here, but I think it's all really fascinating. Definitely agree that Brouwer didn't produce anything of much use to day-to-day mathematicians, but that's sort of Hilbert's (and Turing's) point: practical common sense doesn't seem too impeded by this.

I think as computer scientists we're essentially carrying out a certain mathematical/philosophical program in this debate, fwiw. Turing showed that if you take working computationally very seriously that you will run into open-endedness and time-as-resource constraints very quickly. Programming is a long exercise in discovering just have very seriously you have to take both of those things (interfaces, abstraction on one side, resources, human patience on the other).

Brouwer and intuitionism are subsequently having a bit of a resurgence in mechanized proving. The non-computability of reals shows its ugly head every time someone working in computational optimization has to write `compare_espilon` instead of just `equals`. Or, perhaps even better, every time someone gets bitten by thinking IEEE reals are "mathematical reals".

I also really like to imagine this because I love this idea that each programmer is unknowingly taking very tiny steps along a grand philosophical program. Unromantically it's obviously true, but there's something fun in trying to imagine just how profoundly computers may yet still impact our understanding of the world.