Constructive proof of Euler's formula In most textbooks on the subject I have seen, Euler's formula (by which I mean $e^{ix}=\cos(x)+i\sin(x)$) is proved by applying either differential equations or the power series of sine and cosine. However, any of these two approaches would rely on the derivatives of sine and cosine. However, I have never seen a proof of these derivatives that does not somehow use Euler's formula.
Is it possible to give such a proof? And if it is, which kind of mathematics does it rely on? Does it rely on the definition of sine and cosine based on the unit circle? And if it does, a new problem arises: If we are to define sine and cosine based on the unit circle, we need the concept of radians and hence the concept of arc length. But this, in return, would require a ---- from a constructive POV --- relatively advanced level of integral calculus. And this suddenly makes the derivation of the formula rely on a large amount of mathematics that has to be constructed as well.
 A: Consider the trigonometric circle, having for implicit equation:
$$x^2+y^2=1$$
Compute the arc length, from the point $(1,0)$ to $(x,y)$, which is also the angle, as $r=1$:
$$x\ dx+y\ dy=0$$
implies
$$ds=\sqrt{dx^2+dy^2}=\frac{dy}{\sqrt{1-y^2}}$$
so that
$$s(y)=\int_0^sds=\int_0^y\frac{dy}{\sqrt{1-y^2}}\ \big(=\arcsin y\to y=\sin s\big)$$
At this stage, we must abstain from using the $\arcsin$ and $\sin$ functions as such, as this would create a circular argument.
Let us compute the derivatives of the inverse function, $y(s)$:
$$\frac{dy}{ds}=\sqrt{1-y^2}$$
$$\frac{d^2y}{ds^2}=\frac{d\sqrt{1-y^2}}{dy}\frac{dy}{ds}=-\frac y{\sqrt{1-y^2}}\sqrt{1-y^2}=-y$$
$$\frac{d^3y}{ds^3}=\frac{d(-y)}{dy}\frac{dy}{ds}=-\sqrt{1-y^2}$$
$$\frac{d^4y}{ds^4}=\frac{d(-\sqrt{1-y^2})}{dy}\frac{dy}{ds}=\frac y{\sqrt{1-y^2}}\sqrt{1-y^2}=y$$
and so on.
Clearly, the Taylor development from $s=0$ (i.e. $y=0$) is
$$y(s)=s-\frac{s^3}{3!}+\frac{s^5}{5!}-\frac{s^7}{7!}...$$
Repeating with $x(s)$, we can show that the Taylor development of $x(s)+iy(s)$ formally coincides with the Taylor development of $e^{is}$.
$$x(s)+iy(s)=1+is+\frac{(is)^2}2+\frac{(is)^3}{3!}+\frac{(is)^4}{4!}+\frac{(is)^5}{5!}...$$
The circular argument was avoided by using independent definitions of the trigonometric functions, based on the circle equation, and the fact that computation of the derivatives uses rational expressions only.
UPDATE
When handling the function $s(x)$, you see the strange constant $\int_0^1\frac{dx}{\sqrt{1-x^2}}\approx1.57079632679...$ appear. Denoting it as $\pi/2$ (for instance), we have the identity $e^{i\pi/2}=i$.
A: Many modern texts define the sine, cosine, and exponential function directly in terms of their Taylor expansions. The definition are then very rigorous, requiring very little analysis to prove the basic properties etc. Euler's formula is then easily derived, as you say, through the series. 
This would have been really great except that these definition being very hard to motivate (i.e., why the hell do we take just these coefficients, and then everything works, like magic). So, when I teach these functions properly I usually spend some time on the geometric definitions of the since and cosine function (in terms of the unit circle and radians) but everything is informal. Then one can give a pretty simple proof that the derivative of $\sin$ is $\cos$. The function $\exp$ can be motivated in various ways (i.e., through compound interest or as a solution to $x'=x$). Then you can informally run over the idea of series expansion and obtain (without justification (yet)) the series expansions of these functions, and note the Euler formula. At that point you say: well let's just define these functions and forget about the whole geometric motivation. Better yet, let's remember the geometric motivation and figure out we found a slick way of defining them rigorously without using somewhat vague geometric concepts.  
The thing is also that the definition of the trigonometric functions (when done geometrically) are a bit tricky since they rely on the notion of length, but length is a very subtle thing. It is possible though to define the trigonometric functions in terms of area (but I can't give you a reference I'm afraid). 
A: 
I have never seen a proof of these derivatives that does not somehow use Euler's formula.

$$\sin'x~=~\lim_{h\to 0}\frac{\sin(x+h)-\sin x}h~=~\lim_{h\to 0}\frac{\big(\sin x\cos h+\cos x\sin h\big)-\sin x}h~=$$
$$=~\sin x~\underbrace{\lim_{h\to 0}\frac{\cos h-1}h}_{\cos'0}~+~\cos x~\underbrace{\lim_{h\to 0}\frac{\sin h}h}_{\sin'0}~=~-\sin x~\lim_{h\to 0}\frac{2\sin^2\frac h2}h~+~\cos x~\lim_{h\to 0}\frac{\sin h}h$$

Now all we have to do is prove that $\dfrac{\sin h}h\to1$ as $h\to0$, which can be done using geometry and squeezing:
$\qquad\qquad\qquad$ 
It follows from the figure that $\sin\theta<\theta<\tan\theta~=>~1<\dfrac{\theta}{\sin\theta}<\dfrac1{\cos\theta}$ . By letting $\theta\to0$, the value of the desired limit is thus established.
A: Since I asked the question, I came up with the following solution, which, I think, may be the most beautiful formalisation of a proof of the Euler's formula. It only works, however, if we assume that we already know that $e^{2\pi i} = 1$. If anyone can find a simple proof of this that does not use Euler, say so.
We consider the curve $\gamma\colon\Bbb R\to\Bbb C$ given by $\gamma(t) = e^{it}$ for all $t\in\Bbb R$. It is obviously smooth because $\exp$ is. We define $\cos$ and $\sin$ by Euler's formulas.
Lemma 1: $\gamma$ is a parametrization of a part of the complex unit circle $S^1$.
Proof: We have $\lvert \gamma(t)\rvert =\gamma(t)\overline{\gamma(t)}= e^{it}e^{-it} = e^0 = 1$.
Lemma 2: $\gamma$ is $2\pi$-periodic.
Proof: Since $e^{it}e^{is} = e^{i(t+s)}$ for all $s,t\in\Bbb R$, it follows from the fact that $e^{2\pi i} = 1$, which we assumed to know. (We haven't proved, however, that $\gamma$ could not have a shorter period).
Lemma 3: $\gamma$ paremetrizes all of the unit circle.
Proof: Let $p\in S^1$ be a point on the unit circle. We must show that $\gamma$ hits $p$. Since $\overline{\gamma(t)} = \gamma(-t)$ for all $t\in\Bbb R$, we may assume without loss of generality that the imaginary part of $\gamma$ is $\ge 0$, hence $p\in S^1_+ = \{s\in S^1\mid\operatorname{Im}(s)\ge 0\}$, the upper complex unit circle. It is not hard to show that all points on $S^1_+$ are uniquely determined by their real values, hence we only have to show that $\operatorname{Re}(\gamma)$ takes the value $r:=\operatorname{Re}(p)$. Now the real part $\operatorname{Re}(\gamma)$ is a smooth function $\Bbb R\to [-1,1]$ with $\gamma(0) = 1$, so if it does not take the value $r$ on $[0,2\pi)$, $\operatorname{Re}(\gamma)$ must have a lower bound, hence $\operatorname{Re}(\gamma)(t)\ge b$ for alle $t$ for some $b\in(-1,1)$ (if $b = -1$, $\operatorname{Re}(\gamma)$ would be surjective onto $[-1,1]$ by continuity, which is a contradiction). This is also true for the restriction of $\gamma$ to the compact set $[0,2\pi]$, hence $\operatorname{Re}(\gamma(s)) = b$ for some $s\in[0,2\pi)$. Then $\operatorname{Re}(\gamma'(s)) = 0$. But $\gamma$ has the constant absolute value 1, hence $\gamma$ and $\gamma'$ are perpendicular (differentiate $1 = \langle\gamma,\gamma\rangle$ and get $0 = 2\langle\gamma',\gamma\rangle$); but the only points on $S^1_+$ with a purely imaginary tangent vector are $\pm i$. Hence $p$ is perpendicular to $\pm i$. But this implies that $p = \pm 1$. $p$ obviously cannot be $1$, and if $p = -1$, the same continuity argument as before shows that $\operatorname{Re}(\gamma)$ is surjective onto $[-1,1]$. In either case, we get a contradiction.
Definition 4: Let $p\in S^1$. The angle of $p$ is the (minimal) number $\theta$ in $[0,2\pi)$ such that $\gamma(\theta) = p$.
Now $\cos(\theta)$ and $\sin(\theta)$ are the real and imaginary parts of the number $p$, by definition of $\cos$ and $\sin$. Notice that our definition of angle does not rely on the arc length as defined by integration methods. It is, however, consistent with the angle as defined through arc lengths:
Proposition 5: The angle of a point $p\in S^1$ is the arc length from $1$ to $p$.
Proof: The arc length is, by definition, the length of any surjective smooth curve on $S^1$ from $1$ to $p$; $\gamma\big|_{[0,\theta]}$ is such a curve, where $\theta$ is the angle of $p$. We have that the length of $\gamma\big|_{[0,\theta]}$ is
$$
\ell(\gamma\big|_{[0,\theta]}) = \int_0^\theta\lVert\gamma'\rVert d t = \int_0^\theta 1 d t = \theta.
$$
Hence we have gone from the complex exponential function to the arc length on the unit circle, which was what I requested. Thus if someone has a good argument that $e^{2\pi i} = 1$, we are done.
A: defining $\cos$ and $\sin$ as the projections of a radius vector on two axes separated by a right angle, the derivatives can be computed from the compound angle formulae, which may be proved geometrically.
