Note: This question is inspired by a paper being discussed in the FoM mailing list.
The formal statement Con(PA) is a statement about the existence of a proof code for the derivation of a contradiction is PA, which involves quantification over the numbers of PA. For something to be provable in PA, it would have to hold in all models of PA but as we know, there are nonstandard models. Thus to prove in PA no number codes for the proof of a contradiction in PA it would have to hold in nonstandard models as well. Could it be that some nonstandard model of PA has proof codes which code for proofs of a contradiction yet are not finite under our normal understanding? The paper linked above seems to suggest we can prove in PA that there are no properly finite proofs of a contradiction in PA, yet Timothy Chow in the FoM mailing list seems to think that the paper suggests nothing new.
Could it be that there are proof codes for a contradiction in nonstandard models? Can we gain insight about the consistency of PA by restricting ourselves to proofs of properly finite length?