Is it possible to constructively prove that it is not a decidable set?

@CiaránTaaffe A constructive proof of “is not a decidable set” is an algorithm that, given any potential proof of ”is a decidable state“, exhibits a contradiction in that proof.

@Gilles'SO-stopbeingevil' Thanks, you are correct. Nevertheless, I have not been convinced by the proofs which I have encountered. The central gimmick in the usual proofs is either explicit self-reference or implicit self-reference by diagonalisation. I am grateful for your responses, but I was hoping for some other kind of evidence, perhaps from the field of formal verification. Perhaps I should be asking a different question.

@CiaránTaaffe Constructive proofs of the existence of non-recursive languages can be found on the web (e.g. search Coq Rice's theorem). Self-reference isn't contradictory with constructiveness.

@Gilles'SO-stopbeingevil' Perhaps self-reference is not, but what does it mean for a machine to have itself as a subroutine?

@CiaránTaaffe You've either only seen bad explanations of the proof, or misunderstood them. I've spelled out the proof.

@CiaránTaaffe: the proofs you doubt have been studied thousands of times, formalized dozens of times, checked by machines, and are entirely unproblematic. While ultimately it is a personal matter whether a person finds a proof convincing, the rest of us can only present overwhelming evidence and hope that you will take the effort to understand it. Notions such as "potential vs. actual infinity" play no role here, while self-reference is a central and well understood notion in computer science. There is no mystery here, only misunderstanding.

@Arno The resultant contradiction is not the fault of D. We can see this by removing D from the picture. F(input t): Run [t]('t'), halt. The behaviour of F depends directly on t. Now let's try F(F). F(F) is defined as doing whatever F(F) does. So what does F(F) do? This is an invalid definition. There is a parallel with mathematics here. "x=x" is a valid statement, but an invalid definiton. Mathematicians don't just object to defining "x=x+1" (contradiction) but also "x=x" (self-reference). We cannot define a thing dependent on it's own definiton. But F(F) and [e]('e') do exactly that.

@CiaránTaaffe We are running a program on a string. The fact that the string is the sourcecode of the program doesn't matter. In your example, it is perfectly well defined what F(F) does. It keeps making recursive calls to itself, which never resolve. It thus never reaches the "halt"-command and runs forever.

@AndrejBauer "potential vs. actual infinity" most certainly does play a major role here! My own lecturer on computability theory told me "well there are uncountably many sets, but only countable many TMs". Uncomputability follows directly from "actually infinite sets". Perhaps you had not heard of such a conception of uncomputability before, but now you have. As for "self-reference" Perhaps I should have said "defining things dependent on themselves". I merely used the term because Professor Brailsford referred to it as such in a computerphile video. Sorry for any confusion he caused.

Just because your lecturer gave you one argument that refers to uncountability, that does not mean every argument must incorporate infinity. Look, in mathematics any talk of "potential" vs. "actual" infinity is a bit counter-productive, as these are not technical terms. I answered below with a very specific way of proving the result that does not even need set theory, just arithmetic.

@Arno That would be a very strange way of behaving!! In that case when E('e') tries to build itself and then pass itself to D, it would do the same thing!! Just like you describe F(F) calling itself and not reaching 'halt' when it tries to compile, then E('e') would call itself and not reach D when it tries to compile. Checkmate, my friend.

@AndrejBauer That is exactly why I requested proofs that do not incorporate infinity in my question?!

@CiaránTaaffe E('e') doesnt "try and build it". It just a program applied to a string. We don't run that program. We give that thing to D. Sit down and write this out in a programming language of your choice if you can't wrap your head around this.

@Arno You said "Here, with [s](‘s′) I mean 'consider s as a program, and apply this program to the input given by s considered as a string'" given input 's'. Then you said that precisely this process (which I referred to as "building") results in a recurrent call to [s](‘s′). I am sorry, but you are contradicting yourself. What is the behaviour of F(input t): Run [t]('t') on (F), which does not contradict your claim that E('e') successfully compiles ("considers as a program...appl[ied]...to the input") E('e')?