  Constructive set theory from the very start has a more distinctive foundational vocation and it is bound up with Bishop’s mathematics. In fact, in 1967 Bishop published the book “Foundations of constructive analysis” (Bishop 1967), which opened up a new era for mathematics based on intuitionistic logic (see the entry on  constructive mathematics). The monograph stimulated fresh attempts in the logical community to clarify and formally represent the principles which were used by Bishop, though only at an informal level. First attempts by Goodman and Myhill (Goodman and Myhill 1972) made use of versions of Gödel’s system T (see also (Bishop 1970) for a similar attempt). Myhill, however, reached the conclusion that the resulting formalisation was too complex and artificial (Myhill 1975, 347). Myhill proposed instead a system which is closer to the informal notion of set originally utilised by Bishop and also closer to the set-theoretic tradition. Myhill writes (1975, 347):