Hmm - but isn't there any way to have both "the ability to use the full power of the language at parse time" and still be parseable? If we removed just subroutine prototypes rom the language the proof would not hold any more. So the question is is there a more general proof that does not rely on prototypes?