I'm studying proof theory and type theory, mostly from "Lectures on the Curry-Howard Isomorphism" and Girard's "Proofs and Types" but some things aren't quite clear. In particular, with the regards to Godel's T: I have seen the proof that uses modified realizers in T to provide computational content to proofs in HA. This proof to me does not seem to directly involve the issue of whether terms in T are strongly normalizing. Rather it simply takes as a starting point or axiom that there are no realizers of $\bot$; which is a delicate piece of reasoning because it comes very close to assuming what you are trying to prove.
I understand that by incompleteness that proofs of Con PA cannot be formalized in arithmetic. It seems that here the difficulty comes from the fact that the relation "$M$ realizes $\varphi$" is not arithmetic. But again it is not clear to me what this has to do with normalization.
Is there a direct equivalence betweem strong normalization of a system like Godel's $T$ and the consistency of $PA$? Where can I find a clean proof of this?
(I am aware of the relation between normalization and cut elimination but I would appreciate sources where this is presented cleanly; I have only seen informal explanations. In any case, I don't understand how you would adapt a cut elimination proof to imply the consistency of $HA$ - it's not clear how it generalizes from "pure" first order logic.)