 To do actual mathematics we need more than just intutionistic logic. For Bishop, the building blocks of mathematics were the positive integers (see the quote from Bishop [1967] in Section 3.1 above). Among the early formal systems for BISH were Myhill’s [1975] axiomatic foundation based on primitive notions of number, set, and function; Feferman’s [1975] system for explicit mathematics; and Friedman’s [1977] intuitionistic ZF set theory. The two most favoured formal underpinnings of BISH at this stage are  constructive Zermelo-Fraenkel set theory (CZF),  in Aczel and Rathjen [2010, in Other Internet Resources], and  intuitionistic type theory,  in Martin-Löf [1975, 1984].