In this talk we start by describing weakly extensional Heyting arithmetic in all finite types. We then present Gödel's functional or ‘dialectica’ interpretation of arithmetic, and discuss its soundness proof and the circumstances in which a formula is equivalent to its interpretation.