Two applications of dynamic constructivism: Brouwer's continuity principle and choice sequences in formal topology

In dynamic constructivism the origin of concepts is seen to be a dialectical process between two requirements: convenience of abstractions and faithfulness to reality. The essence of constructivism is then shifted and becomes awareness of the level of abstraction and its uses, rather than a static self-limitation to certain principles. This is perfectly consonant with a minimalist foundation of mathematics, which in particular is based on two different levels, one for computational (intensional) and one for geometrical (extensional) aspects of mathematics. After a short general introduction, dynamic constructivism is illustrated by two specific applications, which exploit formal topology over a minimalist foundation. My (silent) claim is that this attitude could be consonant to Brouwer's spirit (if not letter). Mathematically, it brings = some new light on two controversial topics of intuitionism, since Brouwer's time. I will show under which assumptions Brouwer's principle, saying that all functions on the real numbers are continuous, can be proved and generalized. And I will argue for a rigourous and simple definition of choice sequences.