During Q&A there was a friendly quarrel about 'mainstream' vs 'constructive' maths. I think there's a funny analogy in here, if you let:

    mainstream proof : constructive proof :: program code : machine code

then Kevin is arguing that the idea of actually compiling his beautiful algorithms into machine code is silly, and that compiling program code in general is rather pointless.