This is a largely a question of pedagogy/references, though I may have overlooked some nuance of actual mathematics.

I am planning to introduce the concept of Turing machines and the halting problem to utter novices.

The proofs (or rather proof sketches) of undecidability for the halting problem that I have seen fix a universal Turing machine and vary a program and an input that both reside on the TM's tape. In effect an infinite 0-1 array is formed which is indexed by programs and inputs, with entries indicating whether or not the TM supposedly halts on the corresponding program/input pair. One then employs a diagonal argument.

But it seems more concrete to me to ditch the stored program idiom, let the TM vary instead, and use a TM/input pair for the diagonal argument. It is very easy to produce an explicit enumeration of TMs, and far less so to detail an encoding scheme for a universal TM's tape that allows one to sensibly distinguish the program from the input (of course I know this can be done, but an existence proof is not a great primary approach for very inexperienced students, I think).

So, are there any references that discuss a proof of the undecidability of the halting problem along these lines? (A little part of me actually wonders whether or not I have missed some trivia that obstruct such a proof, because I haven't seen one.)

This is a largely a question of pedagogy/references, though I may have overlooked some nuance of actual mathematics.

I am planning to introduce the concept of Turing machines and the halting problem to utter novices.

The proofs (or rather proof sketches) of undecidability for the halting problem that I have seen fix a universal Turing machine and vary a program and an input that both reside on the TM's tape. In effect an infinite 0-1 array is formed which is indexed by programs and inputs, with entries indicating whether or not the TM supposedly halts on the corresponding program/input pair. One then employs a diagonal argument.

But it seems more concrete to me to ditch the stored program idiom, let the TM vary instead, and use a TM/input pair for the diagonal argument. It is very easy to produce an explicit enumeration of (binary) TMs, and far less so to detail an encoding scheme for a universal TM's tape that allows one to sensibly distinguish the program from the input (of course I know this can be done, but an existence proof is not a great primary approach for very inexperienced students, I think).

So, are there any references that discuss a proof of the undecidability of the halting problem along these lines? (A little part of me actually wonders whether or not I have missed some trivia that obstruct such a proof, because I haven't seen one.)