[I apologize in advance for the fact this post does not rhyme.] Henry Cejtin told me one time that the halting problem was not as cool a foundation for undecidability as this: OPTIMAL-KOLMOGOROV-COMPLEXITY DECISION PROBLEM: Given a program P, decide whether P is shortest-possible. PROOF (BY G.CHAITIN) THIS IS UNDECIDABLE: Assume for a contradiction, that some "is it shortest possible?" decidion-procedure D existed. Modify D (by adding a constant number C of lines of code to it) so that the resulting program D' enumerates all possible computer programs X, until it finds one which is longer than length(D)+C, and which is shortest possible; then D' runs X. Note that D' is now a program shorter than, but equivalent to, X. This contradicts the fact X was shortest possible. Q.E.D.