> I think you're right on the money bringing Turing into this.
Well, his most famous paper, the one in he was first discovered the essence of what computation is (rather than merely asking what functions can be computed by a "definite procedure"), was named On Computable Numbers, and he uses the very problem of the real numbers as a segue into the more general topic of computation.
> 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.
I don't think there is any such bijection (if only for the cardinality argument you mention), but that it turns out (thanks to halting), that lawful and lawless sequences are equally opaque: it is as impossible to determine (using finite means) whether two lawful sequences are equal as it is to determine whether two lawless sequences are, which is all that's required (I think) for the theory. Therefore the same idea that Brouwer had in mind does not really require lawless sequences (which, I think, he wouldn't have introduced if he'd known about halting).
> 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).
It's a bit more complicated, as Turing himself -- in his published conversations with Wittgenstein -- opposed intuitionism as a foundation, believing that math neither has nor requires one true formal foundation. After all, Formalism is also finitistic, and you can just as well use a program to prove a theorem about (classical) real numbers using finite means; there's no need to construct -- i.e. give specific meaning to -- each real number. That was Hilbert's point: it is enough to reason about mathematical proposition in a finitary manner, and there's no actual need to construct the objects in their domain of discourse with finitary means.
> Brouwer and intuitionism are subsequently having a bit of a resurgence in mechanized proving.
Yes, but I think the relationship is more complicated. Again, a mechanical prover can prove classical propositions -- by using deduction rules -- just as it can prove intuitionistic propositions. The resurgence with respect to mechanical provers, as far as I understand, has two reasons: 1. it is easier to create a tiny universal core for a mechanical prover based on intuitionsitic logic, and classical logic can then be built on top of that. 2. much of the research on the theory of functional programming rests on the desire (explicitly stated by Martin-Löf) to unify programming and constructive math. I personally find this approach misguided for various reasons (I'm not a mathematician or a logician, so I see this from a practicing programmer's perspective), but I can understand the appeal.
> there's something fun in trying to imagine just how profoundly computers may yet still impact our understanding of the world.
Oh, absolutely. Once Turing realized that computation is in a very strong sense a fundamental natural phenomenon, he understood the many implications (on logic, AI, biology and physics).