Kleene introduced realizability as a practical semantical interpretation of Heyting Arithmetic (see link for definition). The key result he proved is that provability of $\varphi$ in HA implies the existence of a realizer $n \in \mathbb{N}$ for $\varphi$. Two questions:
Is $n$ computable from the Gödel code of $\varphi$? Or otherwise, is it at least computable from the Gödel code of the proof of $\varphi$ in HA (assuming there is such a proof)?
In what system is Kleene's result proved/can be proved (my interest is mostly in the weakest such system)?