I (think I) understand the enumeration and then diagonalization proof of the undecidability of the halting problem, but I came cross this proof in SICP below, which does not seem to require the enumeration. Did I miss anything?
(define (run-forever) (run-forever)) (define (try p) (if (halts? p p) (run-forever) 'halted))
I suspect this has to do with how a TM is encoded, i.e. the parameter for
try. Being able to encode a TM might require enumeration? But I'm still very confused.