You are being a bit too quick to equate finitism and constructivism. Hilbert was a finitist, but not a constructivist, and Brouwer was a constructivist, but he was not a finitist.
Brouwer's analysis of the continuum depends heavily upon the notion of a "free choice sequence" (aka a lawless sequence). The idea is that a creating subject -- i.e., you or me -- is free to make an unbounded sequence of choices to produce a sequence. At any finite time, you can only have made a finite number of arbitrary choices, but if you wait long enough you can make any number of arbitrary choices. Because these choices are arbitrary, free choice sequences cannot be described as being generated by any finite rule.
This is a constructive process, if you imagine (for example) generating a lawless sequence by throwing dice or from the clicks of a Geiger counter. But it's not a finitist one, because there is no finite data from which a choice sequence can be computed. This let Brouwer retain the idea that a mathematician can only have considered a finite amount of information at any point, without having to make any identification of the real numbers with computable functions.
In terms of complexity, there's an interesting analogy between choice sequences and the question of whether randomization gives you extra power -- the Miller-Rabin primality test lends immense force to the intuition that RP is stronger than P, but we might be centuries from proving it.
Even if we set aside randomness, though, an ultra-finitist/complexity-aware-logic is something that basically every logician I've ever talked to has agreed should exist, except we basically don't know how to do it. It's something that pretty clearly demands more creative insight than technical grunt, and unfortunately imaginative leaps don't come on demand. :/
We need to separate Brouwer's construction of the choice sequences from his philosophical justification for them; in the transition between the two there were just things he couldn't have known. His entire conception of choice sequences was because the mathematician's mind is finite. He couldn't have based his choice sequences on computation because the notion didn't exist yet, but if it had, he wouldn't have needed "lawless sequences". There is just nothing that requires them either in his chosen axioms or in his philosophy -- their salient feature is that one cannot predict their behavior, something that, after Turing, we know is true even for "lawful sequences" but Brouwer didn't. I, therefore, do not think it is correct to say that he wasn't a finitist because he relied on randomness. As far as he knew, randomness was consistent with a finite mind, the finiteness is what mattered to him, and anyway, he cared about undecidability, not randomness, but didn't know the former can exist without the latter.
What is essential to his philosophy is that the only justification for the axioms can come from nature by way of empiricism, and is therefore finite. If you accept Russel's, Brouwer's and Hilbert's belief that mathematics contains Truth, and if you then accept Brouwer's belief that the only source of truth is nature by way of empiricism, you have no choice today but to reject both LEM and induction. It is perfectly fine to work in constructive mathematics, and, in the Turingian sense it is of value, but it is no longer justified by Brouwer's philosophy of mathematical truth. Brouwer would have had to reject today's constructive mathematics on the same grounds he rejected classical mathematics: its axioms are unjustified by nature and empirical observation, even in principle. In fact, I don't think there is any philosophy of mathematics that could distinguish between constructivism and classical mathematics on any reasonable philosophical grounds today.
I would say that Brouwer's philosophy is (with today's knowledge) constructivist and ultra-finitist. BTW, Brouwer was not opposed to formalism as much as he was to logicism, and he even tried to propose a way to reconcile the two ("Intuitionistic reflections on formalism", 1927).
In modern terms, you can identify sequences and automata: a sequence is a current state, plus a transition function giving you the next element of the sequence and the next state. However, if every function is tracked by a computable process, then the transition function must also tracked by a computable process, and so every infinite sequence must be generated by a computable process.
This identification is precisely what choice sequences are used to rule out. If a sequence is genuinely arbitrary, then you cannot describe it up front with a finite amount of data and a finite rule for updating that data. Instead, you have to imagine a mathematician adding a new axiom at each time step about the next element of a choice sequence, and requiring that any constructions they do works uniformly regardless of what axioms may be chosen in the future.
In this picture, the total amount of axiomatic data is actually going up over time, and this is actually important for the results Brouwer proved. In particular, without the axioms for choice sequences, you cannot derive the strong counterexamples, because you need classically-false axioms to prove classically-false theorems (like the continuity of all real-valued functions).
> This identification is precisely what choice sequences are used to rule out.
But you don't need to rule them out -- Brouwer certainly didn't. He just wanted to rule out decidable sequences. It's the undecidability that's important to his result, not arbitrariness, and that's perfectly compatible with automata. He just didn't know about computational undecidability and thought that undecidability requires lawlessness, but it doesn't. In any event, he didn't think randomness violates finitism. That only finite systems can be the source of axioms has been a constant refrain of his. I see that according to Wikipedia's definition of Finitism, he would be a "classical finitist."
> In particular, without the axioms for choice sequences, you cannot derive the strong counterexamples, because you need classically-false axioms to prove classically-false theorems (like the continuity of all real-valued functions).
The continuity of all real-valued functions can be proven with just computable sequences because of undecidability; you just can't do it if computational undecidability hasn't been discovered yet. In fact, it doesn't even become quite "classically false", but can be "embedded" in classical mathematics by restricting the "all": all computable real functions are continuous is a classical theorem. AFAIK, all constructive theorems can be embedded in classical mathematics by restricting them to computable entities. Do you have an example of any result that relies on uncomputable sequences?
> It's the undecidability that's important to his result, not arbitrariness
Undecidability is arbitrariness - to say that, for example, the axiom of choice is independent of ZF is the same thing as saying that there is a arbitrary choice[0] between ZF+C and ZF+!C. Similarly, the sequence[1] G(PA),G(PA+G(PA)),G(PA+G(PA)+G(PA+G(PA))),... requires (at least) one additional arbitrary bit per item.
0: not asserting anything about what makes that choice, though.
1: where G(X) is the Godel sentence, roughly "X cannot cannot prove G(X)"
What I meant was that Brouwer doesn't need lawless sequences; all the results are valid with lawful sequences only. He just didn't know that because he didn't know that lawful sequences can be undecidable. You can call it arbitrary, but it doesn't have to be random, it just needs to be unknowable, which is the case even if it's chosen by a computational rule. It is true that most of the sequences of the kind you presented are not computable, but I don't think any result of Brouwer's is affected.
Brouwer's analysis of the continuum depends heavily upon the notion of a "free choice sequence" (aka a lawless sequence). The idea is that a creating subject -- i.e., you or me -- is free to make an unbounded sequence of choices to produce a sequence. At any finite time, you can only have made a finite number of arbitrary choices, but if you wait long enough you can make any number of arbitrary choices. Because these choices are arbitrary, free choice sequences cannot be described as being generated by any finite rule.
This is a constructive process, if you imagine (for example) generating a lawless sequence by throwing dice or from the clicks of a Geiger counter. But it's not a finitist one, because there is no finite data from which a choice sequence can be computed. This let Brouwer retain the idea that a mathematician can only have considered a finite amount of information at any point, without having to make any identification of the real numbers with computable functions.
In terms of complexity, there's an interesting analogy between choice sequences and the question of whether randomization gives you extra power -- the Miller-Rabin primality test lends immense force to the intuition that RP is stronger than P, but we might be centuries from proving it.
Even if we set aside randomness, though, an ultra-finitist/complexity-aware-logic is something that basically every logician I've ever talked to has agreed should exist, except we basically don't know how to do it. It's something that pretty clearly demands more creative insight than technical grunt, and unfortunately imaginative leaps don't come on demand. :/