Variant of the usual proof method for undecidability of the halting problem 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.)
 A: There is another approach that I find students like. Let $L(n)$ be the length of the shortest program (in some programming language the students know) whose behaviour is to write the number $n$ and stop. Assume there is a procedure that computes $L(n)$. Now write a program that computes $L(1),L(2),\ldots$ in a loop until it finds some $k$ with $L(k)>N$, where $N$ is a constant written into the program, then writes $k$ and stops. By adjusting $N$ to be longer than the length of this program (including the procedure for $L(n)$), you get a contradiction.  So $L(n)$ is not computable.
From that you can do the halting problem: If you could test whether programs will halt, you could compute $L(n)$ just by trying all halting programs in increasing order of length until you find one that writes $n$ before it halts.
A: Although I recognize this is a matter of taste, I do not find it unnatural to fix a TM.
I find the proof by contradiction relatively concrete.  In that proof structure, the start is: Suppose there exists, for the purposes of contradiction, a TM $T_1$ that determines if any other halts.  Then we could construct a TM $T_2$ that accomplishes the impossible.  So $T_1$ cannot exist.
This is the proof in Hopcroft and Ullman's Formal Languages and their Relation to Automata, pp. 108-9.  
Perhaps you would find worthwhile the variant on this proof structure used in Aho and Ullman's Foundations of Computer Science, p. 750.
Here they do not use TMs, but rather just programs, calling $T_1$ the "decider" program, reaching the conclusion that no such decider can exist via a "complementer" program.
One can present a few wiring diagrams using the decider and complementer programs as black boxes
to make the contradiction clear.  Not-halting can be equated with infinite loops.
If your utter novices are programmers, this approach can
be more convincing than an indexed diagonal argument.
       

A: The proof sketch on Wikipedia uses a very common method (the same as in Proposition 4.4 of Soare's book) that relies only on universality of the computation system and on closure properties of the class of computable functions. It won't make any mention of Turing machines directly, or any other specific model of computation.  This is what I think of as the "usual" approach, which could be only half-jokingly described a "get away from Turing machines as fast as possible". The motivation is that computability theory is the study of computable function, not Turing machines. 
