 Kleene used a variant of number-realizability to prove \(\mathbf{HA}\) satisfies the Church-Kleene Rule; the same argument works for \(\mathbf{HA}\) with MP or CT, and for \(\mathbf{HA}\) \(+\) MP \(+\) CT. In Kleene and Vesley [1965] and Kleene [1969], functions replace numbers as realizing objects, establishing the consistency of formalized intuitionistic analysis and its closure under a second-order version of the Church-Kleene Rule.