Chaitin's elegant programs I need help to understand Chaitin's elegant program proof. An elegant program is the shortest program that produces a given output.
Here is the proof:

Construct a program $B$ that takes as input a number $N$ and enumerates all possible programs $P_k$ longer than $N$. $B$ runs the elegance tester $\mathrm{ET}$ on each enumerated program $P_k$ in turn until it finds some $P_k$ which $\mathrm{ET}$ claims is elegant. $B$ then runs that $P_k$, thus producing the same output as that $P_k$.
Lemma: B must produce some output.
Proof: There are an infinite number of elegant programs, as noted earlier. So if $\mathrm{ET}$ works as assumed, $B$ must eventually find one of those elegant programs whereupon it will produce that program's output.
Now run $B$ with $N$ set to $|B| + 1$ (See note 1). (This is the &quot;threshold size&quot; mentioned in the theorem.) $B$ now will produce the same output as some program $P_k$ which $\mathrm{ET}$ claimed was elegant. But $P_k$ is longer than $B$, so $P_k$ cannot be elegant because $B$, which is shorter, produced the same output. Therefore, $\mathrm{ET}$ was wrong when it claimed $P_k$ was elegant. QED.

My question is: The proof begins with a program $B$ that is a program &quot;that takes as input a number $N$ and enumerates all possible programs $P_k$ longer than $N$&quot; But because of the halting problem such a program is not possible, so the proof starts dead? There is something I'm not understanding here.
The algorithm $B$ is described in a mildly sloppy way. You can look at it as a two-step process:


Find suitable $P_k$.
Run $P_k$.


Now, step 1 can be done one program at a time since the set of all programs is recursively enumerable and we assume that a recursive (and total) elegance tester $\mathrm{ET}$ exists. Note that we use $\mathrm{ET}$ as an oracle.

So, the algorithm is this:

def B(N,x)
  E = program_enumerator

  do
    P = E.next
    if ( length(P) &lt;= N )
      continue
  while ( !ET(P) )

  return P(x)
end


Why is this a proof? We call the underlying technique proof by contradiction. Here is what happens:


Assume that a general, total elegance checker $\mathrm{ET}$ exists.
Under this assumption, construct a (computable!) program $B$ that is equivalent to a program $P$ so that $B$ is smaller than $P$ but $\mathrm{ET}$ says that $P$ is elegant (i.e. smallest).
Since this is a contradiction, the assumption has to be false; that is, such an elegance checker can not exist.