Some points in formal topology. (Q1427787)

It is now more than fifteen years since the appearance of the author's `first communication' on formal spaces, a constructive and predicative approach to general topology designed to be interpretable in Martin-Löf's type theory. The present paper has three main aims, which are developed in three broadly independent sections: first, to survey the progress that has been made since then in developing traditional notions of topology in the formal setting; secondly, to provide publicity for what the author calls `the basic picture', which is a newer and more symmetric way of looking at the relationship between points and open sets, still under development by the author and S.~Gebellato; and finally, in a section less mathematical and more philosophical in character, to present the author's understanding of how and why one should seek to develop mathematics in a constructive context.