Comment by doctor_phil

I agree, producing a lower bound is possible. It's practically very hard to give a good lower bound though. Many programs do not terminate, so we don't know if they do produce the right output eventually. In practice the best that has been done on Turing machines is that we have now proved which 5-state machines halt and which don't. So proving any lower bounds larger than that is practically impossible.