I think I agree with others that the diagonalization argument is constructive, although from what I can tell there is some disagreement about this in some circles.
I mean, assume that we're looking at the set of all decidable languages. I can construct an undecidable language using diagonalization. It's worth noting that I don't consider "constructivism" and "finitism" to be the same thing at all, although historically I think these were related arcs.
First, I think everybody - even constructivists - agree that the set of decidable languages is countable. Since the set of Turing machines is countable (we can encode all valid TMs using finite strings), this agreement follows pretty easily.
Since the set of decidable languages is countable, we can assume some enumeration of these languages: $L_1, L_2, ..., L_k, ...$. Here's a procedure that will generate a language not in the set:
- Consider the string $0^i$.
- If $0^i \in L_i$, then our language should not contain $0^i$.
- If $0^i \notin L_i$, then our language should contain $0^i$.
After the $n$th step, our language cannot be any of the languages $L_1, L_2, ..., L_n$. After an arbitrary (or potentially infinite) number of steps, we can't have found a language in the set to match the one we've just constructed.
So technically, we've constructed a language that is "not decidable"; whether a constructivist would argue that "not decidable" shouldn't be confused with "undecidable" is an interesting question, but one which I am ill-equipped to answer.
To clarify, what I think this demonstrates is the following: we can constructively prove that there exist languages not decided by Turing machines. How you choose to interpret that within a particular framework is a harder question.