Here are two well known facts, which put together leave me confused. 


First, it's well known that intuitionistic logic is the logic of constructive mathematics. From every intutionistic proof, you can extract an algorithm which will compute the witness to that theorem (i.e., the famous "existence principle" of intutionistic logic). 


Second, it's also well-known that topologies give rise to models of intuitionistic mathematics. We can equate propositions with open sets, and then the fact that a topology is a Heyting algebra gets us off to the races. (Caveat: this is an oversimplification.)


In fact, you can get pretty far with the dictionary "computability is continuity" -- which is precisely what puzzles me!


Intuitionistically, we can construct the real numbers pretty much as usual, eg via Cauchy sequences, which can be viewed as functions $\mathbb{N} \to \mathbb{Q}$ subject to the usual conditions. Now recall that classically, the only continuous functions $f : \mathbb{R} \to \mathbb{Z}$ are the constant functions. So according to this dictionary, we should not expect to give an intuitionistically valid function which computes the integer part of a real number. 


So far, everything makes sense. For example, the Cauchy sequence $0, 0.9, 0.99, 0.999, \ldots$ has $1$ as its limit, but given a black-box $f : \mathbb{N \to \mathbb Q}$, we can't tell that it's this sequence without looking at every $f(n)$ -- which is obviously uncomputable. 


However, suppose that we have in our hand an actual computer program of type $\mathbb{N} \to \mathbb{Q}$ (say, in Haskell), which we happen to know represents a Cauchy sequence. We can actually run this program, and use some prefix of the Cauchy sequence to print something close to the integer part of the real to the computer screen. This operation obviously isn't a *function* on reals, since it can give different results for different representations of the same real. For example, our program might print "1" for the Cauchy sequence $1, 1, 1, \ldots$, and "0" for the Cauchy sequence "$0.9, 0.99, 0.999, \ldots$". But equally obviously this a perfectly sensible *computer program* to write. 


So that's my question: what *is* this operation, and how can we axiomatize its logical behavior? (What kind of crazy gadget doesn't respect equality!?) 



What happens when we print the digits of a real number?
[**Edit:** Following Carl Mummert's comments, I have improved the part about transformation of Cauchy sequences to digit expansions. Thanks to Carl for interesting observations.]


Your question is best divided into two subquestions:


1. Does every real number have a digit expansion?
2. What is the nature of the "process" of going from a real number to its digit expansion,
assuming it has one.


For the purposes of this discussion let us say that the real numbers are defined a la Cauchy, i.e., $\mathbb{R}$ is the metric completion of $\mathbb{Q}$ equipped with the Euclidean metric. Let me also assume countable choice, so that $\mathbb{R}$ can be shown to exist. In particular, we can take $\mathbb{R}$ to be the set of Cauchy sequences quotiented by a suitable equivalence relation. (I am talking informal intuitionistic mathematics here and do not want to tell you what formal system I am in, but if you force me, I can tell you about various possibilities.)


We need to be careful about what is understood by "digit expansion" of a real number. Digit expansions are special kind of a Cauchy sequences: they are monotone and have a fixed rate of convergence. We have the following observations, none of which is hard to establish (assuming countable choice):


* for every Cauchy sequence there exists one with a fixed rate of convergence (say the
$n$-th term is within $2^{-n}$ of its limit), but a function mapping from the former
to the later cannot be shown to exist.
* every Cauchy sequence with a fixed rate of convergence (let me call such *fast* Cauchy sequences) has a monotone fast Cauchy sequence, and there is a function mapping the former to the later, as pointed out by Carl in the comments.
* a decimal digit expansion is an infinite sequence, i.e., a member of $D = \lbrace 0, 1, \ldots 9\rbrace^\mathbb{N}$. We cannot prove constructively that every monotone fast Cauchy sequence has a corresponding digit expansion (again, by a continuity argument).
* if we try to weasle out of the problem by taking only those reals which have a decimal digit expansion, then basic operations such as addition and multiplication cannot be shown to exist because they would be discontinuous.
* as is well known, if we allow *negative* digits so that a digit expansion is a member of $\lbrace -9, -8, \ldots, 8, 9\rbrace^\mathbb{N}$ then every Cauchy sequence has a corresponding digit expansion, but now every real has very many digit expansions.


So I am going to assume that by "digit expansion" you mean one which can contain negative digits (otherwise your premise that every real has an expansion cannot be established). As you notice, there is no continuous map from reals to (negative) digit expansions. Nevertheless, one can write a program which takes a real number (represented by a rational Cauchy sequence with an explicit modulus of convergence, or some other equivalent form, such as a sequence of ensted intervals with rational endpoints) and produces *one* of its digit expansions. Such programs can be understood in several ways:


1. As realizers for the statement $$\forall x \in \mathbb{R} . \exists d \in D . \;\text{$d$ is digit expansion of $x$}.$$ This is my favorite. When we reason about real numbers in analysis, we rarely talk about digit expansions, so it does not matter if the computation of a digit expansion appears only implicitly as a realizer for a $\forall\exists$ statement.
2. We can formalize a distinction between an *operation* and a *function*. The former
 can be *intensional*, i.e., it does not have to repsect the equality of its domain,
 while the later must be *extensional* so that it maps equals to equals. This introduces
 certain subtleties that only logicians can appreciate. In this setting, the program
 is an operation which is not a function.
3. Such programs can be seen as realizers witnessing the totality of a *multi-valued*
 function that maps a real to the set of its digit expansions. Such a map is easily seen to exist. This is more manageable
 than option 2 and is popular in Type Two Effectivity.


In practice, you cannot hope to implement reals in such a way that each real receives only one representation. Even having finitely many representations is out of the question – some reals will necessarily have infinitely many representatives, or something will go wrong (arithmetical operations won't be computable, or the structure won't be closed under limits of (computable) Cauchy sequences, or the strict linear order won't be semidecidable). Classical decimal digit expansions are *not* computable, even though every single computable real has a decimal digit expansion. This shows the importance of thinking about *spaces* as whole entities, rather than each of its points in isolation. Or to be even more blunt: spaces are *not* determined by their points!


