 (d) Errett Bishop’s novel (informal) approach to constructive analysis (1967) made a great on impression on mathematicians with constructive leanings. In it, he dealt with different kinds of mathematical objects (numbers, functions, sets) as if they were given by explicit presentations, each kind being equipped with its own germane “equality” relation conceived in such a way that operations on them would lead from representations to representations respecting the equality relation. An important ingredient that made Bishop’s constructivism workable is the systematic use of witnessing data as an integral part of what constitutes a mathematical object. For instance, a real number comes with a modulus of convergence while a function of real numbers comes equipped with a modulus of (uniform) convergence. In his explicit mathematics, Feferman (1975, 1979) aims (among other things) at formalizing the core of Bishop’s ontology. Explicit mathematics is a theory that describes a realm of concretely and explicitly given objects (a universe U of symbols) equipped with an operation \(\bullet\) of application in such a way that given two objects \(a,b\in U\), a may be viewed as a program which can be run on input b and may produce an output \(a\bullet b\in U\) or never halt (such structures are known as partial combinatory algebras or Schönfinkel algebras). Moreover, some of the objects of U represent sets of elements of U. The construction of new sets out of given sets is either done explicitly by elementary comprehension or by a process of inductive generation. If one also adds principles to the effect that every internal operation (given as \(\lambda x.a\bullet x\) for some \(a\in U\)) which is monotone on sets possesses a least fixed point one arrives at a remarkably strong theory (cf. Rathjen 1998, 1999b, 2002).