The Curry-Howard correspondence allows rephrasing the intuitionist position as: the proposition expressed by a formula of Heyting Arithmetic is the type of its proofs

It seems to be Kreisel who introduced the slogan ‘formulae as types’, with Martin-Löf responsible for the more widespread ‘propositions as types’ slogan (See again, Wadler, 2015). In the philosophical context, ‘proposition’ is often used to mean something like the meaning of a sentence, i.e. of a formula of a certain sort. Using this terminology, a widespread intuitionist position is that that the proposition expressed by a formula is the set (or species, for the intuitionist) of all proofs of t