I'm just a curious outsider when it comes to constructive mathematics, but it seems to me that it is not possible to actually construct non-analytic functions. It seems that the classical counterexamples of step functions, absolute value function, and bump functions cannot be defined constructively. Am I correct or is it possible to actually exhibit a non-analytic function?
I would prefer not to assume any choice principles (dependent choice, countable choice etc.).
The absolute value function can certainly be defined for the Cauchy real line or Dedekind real line.
For the Cauchy real line, it's easy: given a sequence $x_n$ send it to $|x_n|.$ This is a well-defined map of Cauchy sequences.
For the Dedekind real line, the lower bounds are any rational $r$ such that $r<x$ or $r<-x,$ and the upper bounds are any rational $r$ such that $x<r$ and $-x<r.$ To show this defines a Dedekind cut we should show it is "located", i.e. for any rationals $a<b,$ either $a$ is a lower bound or $b$ is an upper bound (a sort of limited excluded middle). The interesting case is when $0<a<b.$ Since $x$ is located we know that either $a<x$ or $x<b,$ but also that either $-b<x$ or $x<-a.$ Either of $a<x$ or $x<-a$ imply $a<|x|,$ and in the other cases we have $|x|<b.$
This covers constructive analysis as pioneered by Bishop.
Similarly $f(x)=\begin{cases}0&x\leq 0\\e^{-1/x}&x>0\end{cases}$ can be defined constructively i.e. there is a constructive definition which is classically equivalent to the classical definition. I'll just work with Dedekind cuts.
A rational $r$ is a lower bound of $f(x)$ if $r<0$ or if $r<e^{-1/a}$ for some positive rational $a<x.$ A rational $r$ is an upper bound of $f(x)$ if $r>e^{-1/b}$ for some positive rational $b>x.$
To show $f(x)$ is located, consider a rational interval $a<b.$ If $a<0$ then $a<f(x).$ Otherwise, by continuity of $\exp$ there are rationals $0<a'<b'$ with $a<e^{-1/a'}<e^{-1/b'}<b.$ That's just a statement about rationals so there aren't any constructive subtleties. Since $x$ is located, either $x<b'$ or $a'<x.$ If $x<b'$ then $f(x)<b.$ If $a'<x$ then $a<f(x).$ In all cases we have shown $a<f(x)$ or $f(x)<b$ as required.
A more general construction is that a function on $\mathbb Q$ that is uniformly continuous on bounded sets extends to $\mathbb R.$ The proof is just the usual proof for a metric space completion, though with a bit more care if trying to avoid countable choice.