Turing proved that within any formal (or mechanical) system, not only are there functions that can be given a finite description yet cannot be computed by any finite machine in a finite amount of time, but there is no definite method to distinguish computable from noncomputable functions in advance.
