is there a constructive proof of the existence of a language which isn't recursive (without invoking infinities)?
We can write a computer program that will enumerate all halting computer programs. It seems that you are happy to accept accumulating the output of program into a (potentially infinite) set. Thus, you accept &quot;all halting computer programs&quot; as a valid set. It is, however, not a decidable set.
The standard proof of the undecidability of the Halting problem is constructive. Since we are proving a negative statement, a constructive proof is going to start with the assumption that it were decidable and going to derive a contradiction. Note that a decider by definition will answer either &quot;yes&quot; or &quot;no&quot; on any input, we can thus do the case-distinction in the usual proof of the undecidability of the Halting problem without having to involke the law of excluded middle.
Alright, so let us have a look at how exactly to prove that the Halting problem is undecidable. Bob claims the Halting problem is decidable, and we prove him wrong. Since Bob claims decidability, we can make him tell us what program he thinks does the job. Bob has to give us a program D, and the assurance that on any input w, the computation D(w) will halt and answer either &quot;true&quot; or &quot;false&quot;.
Now, consider the following program:
E(input s)
   While {D([s]('s')} {do nothing}
   halt

Here, with $[s](`s')$ I mean &quot;consider s as a program, and apply this program to the input given by s considered as a string&quot;. This may feel weird, but since we have received s, we can obviously copy it and so on.
Now, modulo knowing what D is (and that's Bob's responsibility, not mine), we have a concrete piece of code up there. Call that piece of code &quot;e&quot;. We can again treat e both as a program (which takes an input) and as a string. In particular, it makes sense to consider $[e](`e')$ again, which is the program e run on the string e as input.
Bob has claimed that running $D([e](`e')$ will answer either true or false, and that this answer is about whether the computation $[e](`e')$ ever halts. Since Bob so kindly provided the case distinction for us, we can exploit it.
If $D([e](`e')$ answers &quot;true&quot;, then in the computation that happens when we run E('e') we can never escape the while-loop, so it can't halt. Bob is wrong.
If $D([e](`e')$ answers &quot;false&quot;, then E(`e') never enters the loop, but halts straight away. Bob is wrong, again. We won.