
> 
> What are some good introductory references to constructive mathematics for non-specialist mathematicians?
> 
> 
> 


I would like to learn more about constructive mathematics, just to improve my general mathematical knowledge, but I have some difficulties in finding good references for non-specialists. Are there introductory texts including:


* a rough description of the main motivations and of the history of the field;
* a discussion of the different meanings given to "constructive";
* explicit examples of constructive vs. non-constructive proofs;
* a discussion about what one looses compared to "classical" mathematics?


Of course, I do not necessarily expect a single text satisfying all these conditions, a collection of a few references would do the job.



Initiation to constructive mathematics
I have a soft spot for *Constructivism in Mathematics: An Introduction* (2 volumes) by Troelstra and van Dalen as an overview. And for what one loses compared to classical mathematics (as well as its historical importance), it's probably worth going straight to Bishop's *Foundations of constructive analysis*.


However, an important thing to be aware of when reading older and historical works is that they may give a misleading impression of constructivism as currently practiced. Historical overviews such as Troelstra-van Dalen or Bridges-Richman will often spend time contrasting schools of constructivism such as Brouwer's intuitionism, Markov's constructive recursive mathematics, and Bishop's constructive mathematics. This is certainly interesting and historically important, but in my (humble) opinion, the trend of the future in constructivism is towards "neutral" constructive mathematics, which historically was a bit of a latecomer.


The three historical "big schools" all assume various principles that deviate from neutral constructivism, some of which are even classically contradictory. While some of those principles (notably ones like Markov's principle and countable choice, which are weak "computable" forms of LEM and AC and in particular are consistent with classical mathematics) are still in wide use today, it's become more fashionable to at least notice when they are used and attempt to avoid them if possible.


One important reason for this is that neutral constructivism is valid internal to any elementary topos, whereas these additional principles are not. Topos theory has also led to important insights into the best way to do mathematics constructively, such as the use of *locales* as a good notion of "space".


Thus, I would recommend supplementing your historical reading with some more modern work. Bauer's [Five stages of accepting constructive mathematics](https://www.ams.org/journals/bull/2017-54-03/S0273-0979-2016-01556-4/) cited in the comments is an excellent start. But unfortunately, I don't know of a good book-length work to follow it.


One of my own early introductions to constructivism was a course on constructive locale theory given by Peter Johnstone, much of which became Part C of *Sketches of an Elephant*; but that may be a bit difficult to follow without some background in category theory and topos theory (such as obtained from Parts A and B). The [HoTT Book](https://homotopytypetheory.org/book/) also includes some explanation of modern approaches to doing mathematics constructively, particularly chapters 10 and 11 (plus a few remarks in the introduction); but, again, it may be hard to get there without slogging through chapters 1-9. And of course there is Taylor's [Practical foundations of mathematics](http://www.paultaylor.eu/%7Ept/prafm/index.html), which has many nice features but which Peter Johnstone famously called "the book of which *Mathematics Made Difficult* was a parody". So overall I think there is room here for someone to write a good book.


