 The traditional route taken by mathematicians wanting to analyse the constructive content of mathematics is the one that follows classical logic; in order to avoid decisions, such as whether or not a real number equals 0, that cannot be made by a real computer, the mathematician then has to keep within strict algorithmic boundaries such as those formed by recursive function theory. In contrast, the route taken by the constructive mathematician follows intuitionistic logic, which automatically takes care of computationally inadmissible decisions. This logic (together with an appropriate set- or type-theoretic framework) suffices to keep the mathematics within constructive boundaries. Thus the mathematician is free to work in the natural style of an analyst, algebraist (e.g., Mines et al. [1988]), geometer, topologist (e.g., Bridges &amp; Vîță [2011], Sambin forthcoming), or other normal mathematician, the only constraints being those imposed by intuitionistic logic. As Bishop and others have shown, the traditional belief promulgated by Hilbert and still widely held today, that intuitionistic logic imposes such restrictions as to render the development of serious mathematics impossible, is patently false: large parts of deep modern mathematics can be, and have been, produced by purely constructive methods. Moreover, the link between constructive mathematics and programming holds great promise for the future implementation and development of abstract mathematics on the computer.