Computational intuition on discontinuity I'm trying to understand what continuity, as in topology, intuitively is. The thing that got me thinking is that, it seems usually hard to define functions that are discontinuous. In other words, most natural (i.e., written down by chaining elementary operations) functions on $\mathbb{R}$ are continuous.
It is well-known that in Brouwerian intuitionism, all functions are continuous and this seems related to the fact that functions that are usually pointed out as examples of discontinuous functions in classical mathematics are a bit bizarre. Let me give an example: when I go to the Wikipedia page classification of discontinuities, I see the following function:
$$ 
f : \mathbb{R} \rightarrow \mathbb{R}\\
f(x) = \begin{cases}
  x^2   & \text{for}\ x < 1 \\
  0     & \text{for}\ x = 1 \\
  2 - x & \text{for}\ x > 1.
\end{cases} $$
It is not clear to me how this function comes to exist in the first place. How is equality on the real numbers defined? How do we compute the result of the question $x = 1$? As far as I know, equality on real numbers is not a decidable operation so I'm befuddled every time I see a function defined by cases by checking equality of real numbers. I have tried looking for answers but it seems that these kind of questions are not spelled out precisely in mainstream resources. I would appreciate reading suggestions though!
A simple summary of my question is this: I do not fully understand the relation of the continuity principle in intuitionistic mathematics to the existence of discontinuous functions in classical mathematics. Would I be correct if I said that discontinuity (speaking of the standard topology of real numbers) arises when functions are defined by invoking classical principles such as those allowing us to decide equality of real numbers? If there is any truth to this hunch, can someone explain it precisely?
PS: sure, there is the very natural-looking function $x \mapsto x / (1 - x)$ that is discontinuous due to undefined behaviour but this is essentially not even a function. As far as I know, functions in classical mathematics are defined as relations that are total and deterministic but this thing is not even total as $f(1) \notin \mathbb{R}$ although $1 \in \mathbb{R}$ so it befuddles me even more that we speak of its discontinuity as if it were a proper function in the first place. In type theory, it would clearly not be a function and I wanted to note therefore that this is not the kind of counterexample I am interested in.
 A: For Brouwer the real numbers are not the same as "our" real numbers. That sort of explains the continuity result, I think. A real number is never finished in his idea. Think of a real number roughly as a "recipe" for producing as many digits of it as you like. If you cannot do that, the number is not "well-defined".
So if $f(x)$ (for $x$ a real number (he uses "fans" IIRC)) to be a well-defined real, this means there must be a procedure to determine $f(x)$ up to $1000$ digits (say) by  a recipe that only uses finitely many (maybe $2000$) digits of $x$ etc. This sort of intuitively implies continuity right away. It is just by nature of what a function on "reals" is. You cannot tell in finitely many steps for sure whether a real is $<1$ or $=1$ in all cases (e.g. after seeing $10000$ 9's in $0.99\ldots$' you cannot decide yet). So such a case definition as your first example is not well-defined for intuitionistis mathematics. this blog post might be relevant reading.
BTW, $\frac{x}{1-x}$ is a perfectly fine continuous function from $\Bbb R\setminus \{1\}$ to $\mathbb{R}$. The domain matters. 
A: Here is the requested alternate answer.
Regardless of any underlying justification or interpretation, the formal reason why you can define discontinuous functions classically is excluded middle. If you read $$P ∨ ¬P$$ constructively, the principle is, "all propositions are decidable." So, for instance, your (correct) observation that there is no computational procedure for deciding equality of (computable) reals holds no force, because functions are allowed to be defined by cases on a disjunctive proposition, and $$x \# 1 ∨ ¬\ x \# 1$$ being true is just a principle we have accepted classically (where $\#$ is apartness, which is the fundamental relation on constructive reals; I believe $x = y$ is equivalent to $¬\ x \# y$, while $¬\ x = y$ is weaker than $x\#y$; $x\#y$ is also equivalent to $x < y ∨ x > y$, I think).
Another possible way to think about it is that we can define your function by modifying the domain, similar to the way we would modify the domain for $$x \mapsto \frac{x}{1-x}$$ We could say that your function actually has type: $$\{x \in \mathbb{R}| x < 1\} ∪\{x \in \mathbb{R}| x = 1\} ∪ \{x \in \mathbb R| x > 1\} → \mathbb R$$ or perhaps $$\{x \in \mathbb R | x < 1 ∨ x = 1 ∨ x > 1\} → \mathbb R$$
The important part is that in a constructive system, these domains are not the same as $\mathbb R$, they are like sets of real numbers equipped with additional information. But classically, people have decided that this information is trivial for whatever reason, so these collapse to the real numbers, and your function can just be defined on the reals directly. Another example of this sort of idea is given here, where in synthetic differential geometry, one works with the smooth reals, and any lack of smoothness in a function must be explained by dividing the domain into the pieces on which it is smooth (and even some constructively definable functions are not smooth).
