 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 the formula. Given that different provable formulae will correspond to different types, the CH correspondence allows us to rephrase this ‘syntactico-semantics’ position as: the proposition expressed by a formula of HA is the type of its proofs, where ‘type’ is not a straightforward synonym for ‘set’ or ‘species’ but the notion from \(\lambda\)-calculus. As noted, this calculus is a formal system with rich interconnections with programming and computer science and readings in which the instances of types are purely syntactic, for example proof-theoretic entities. Hence the meaning of a formula, the proposition expressed, on such readings, does not represent a reality distinct from the linguistic system in which the formula occurs. 