The germs of pointfree topology can already be found in some remarks by Whitehead and Russell early in the century. For a detailed account of the historical roots of pointfree topology cf. \cite{J} (notes on ch. II), and \cite{Coq}.
The basic algebraic structure for pointfree topology is that of frame, or equivalently locale, or complete Heyting algebra, that is, a complete lattice with (finite) meets distributing over arbitrary joins. This is the order structure determined by the opens of a topological space with respect to set-theoretic inclusion. A frame can thus be seen as a generalized topological space.
The study of frames in category theory has been undertaken in the field known as {\em locale theory}. We refer to \cite{J} and references therein for this extensive direction in the development of pointfree topology.
Martin-L\"{o}f and Sambin introduced {\em formal topologies} in \cite{S} as an alternative approach to poinfree topology, in the tradition of Johnstone's coverages and Fourman and Grayson formal spaces \cite{FG}, but using a constructive set theory based on Martin-L\"{o}f's type theory (cf. \cite{ML1}).
Formal spaces and their effective presentations have been investigated in \cite{Si} in a classical recursion theoretic setting.
Pointfree topology has also been used for the semantics of computation, via the notion of information system (\cite{Sc,ML3,Vi,SVV}). In \cite{D} (pointfree) topological models have been applied to completeness of intuitionistic logic.
The basic idea of pointfree topology of considering the opens, or approximations, as primitive, is here worked out to obtain a constructive definition of the continuum in the framework of formal topology.
We give an account of all the basic notions of formal topology needed here and introduce the formal topology of intervals with rational endpoints, following an idea already in \cite{J} (also developed in topos-theoretic terms in \cite{V}). The formal points of this topology lead, through a natural construction, to our notion of continuum. Arithmetical operations are defined and an order relation giving rise to an apartness relation is studied in detail.
From a constructive point of view formal reals are not order complete: this property only follows if we assume classical logic. Else, order completeness is obtained by suitably weakening the locatedness of formal reals, following a procedure typical of intuitionistic mathematics (cf. \cite{T}).
As a further confirmation of the correctness of our construction, we show how to obtain, by assuming classical logic, extensionality of the topology of formal reals. This means that the new pointfree space and the point-set one are classically equivalent.
In order to develop constructive analysis, a natural notion of Cauchy sequence is introduced and Cauchy completeness is proved. Moreover, very elementary and constructive proofs of some basic results of analysis, like the Baire theorem and the Cantor theorem, are obtained.
Finally, our notion of reals is shown to correspond to Bishop reals and to Dedekind cuts in their usual constructive treatment, and is compared with Martin-L\"of's maximal approximations.
We emphasize that, from the classical point of view, formal reals are equivalent to the usual reals, so that nothing is lost. What is gained is the possibility of using formal pointfree methods that permit to constructivize results of classical mathematics (cf. \cite{CCN,CN,CS,N,NV,S1} for other examples, also outside analysis) and to pursue the project of machine-implemented formalization of analysis (cf. \cite{C,hhbimpl}).