  The constructive approach to mathematics has the advantage that witnesses can
be extracted from statements of existence and theorems can be unwound to give
algorithms. Even better, constructive theorems can be interpreted in any topos,
giving many different results for the price of one. On the other hand, you
might have heard that fundamental results from topology such as Tychonoff's
theorem or even the intermediate value theorem do not hold constructively,
which can make the price of constructive theorems seem rather steep. However,
almost all of these pathologies disappear if we take the pointfree approach to
topology, in which spaces are studied algebraically and logically through their
lattices of opens without reference to a predefined underlying set of points.
In fact, this perspective also sheds light on aspects of constructive
mathematics that might at first appear to have little to do with topology.
These notes provide a gentle introduction to the main aspects of constructive
pointfree topology and some of its applications.
