Can a proof of the work-energy theorem be made, that doesn't use Leibniz notation to cancel differentials? I've been doing some reading, and even though many people say different things, i think i'm pretty confident in saying that we can't treat differentials as fractions. In some scenarios it works out (chain rule), but in others it will not. Leibniz notation is still notation. It's just very suggestive of the math going on.
Im trying to prove the work-energy theorem, and this is my progress so far:
$$\int F*ds   =>  \int ma*ds  =>  m\int a*ds$$
If acceleration is integrated w.r.t ds, then it must be a function of ds too. We also know that ds, the position, must be a function of time. $$m\int a(s(t))*ds(t)  => m\int \frac{d}{dt}[v(s(t))]*ds(t) $$
With the chain rule, this gives me: $$m\int v'(s(t)) *v(t)*ds(t)$$  
And this is where i'm stuck. I can't seem to find a way to integrate this, especially since i haven't really seen an integral like this before. Time t seems to be the independent variable, but it is still integrated w.r.t ds. All proofs ive found do the following:
$$m\int \frac{dv}{ds}*\frac{ds}{dt}*ds => m\int v*dv => m\frac{v^2}{2}$$ And since this integral was defined to be evaluated from a point A, to point B, we measure a difference in kinetic energy.
But i'm not okay with that proof. We can't just treat differentials as fractions whenever we feel like it. We can say that $$ \frac{df}{dx}=\frac{df}{dv} * \frac{dv}{dx}$$ not because the $dv's$ cancel out, but because of the chain rule (since this is just the chain rule written in Leibniz notation). This proof of the work energy-theroum clearly is correct. What is it that allows us to cancel out these fractions in this scenario? What special rule or derivation makes us certain that canceling out $ds$ is a valid step.
Any help is greatly appreciated. Have a good day! 
 A: Yes.
\begin{align}
 \mathbf{F} & = m\mathbf{a} \equiv m \ddot{\mathbf{x}} & \mathrm{definition}\\
 \int \mathbf{F}\cdot \operatorname{d}\mathbf{x} & = m \int\ddot{\mathbf{x}}\cdot \operatorname{d}\mathbf{x} & \mathrm{path\ integrate\ both\ sides} \\
 \int \mathbf{F}\cdot \operatorname{d}\mathbf{x} & = m \int_{t_0}^{t_f}\ddot{\mathbf{x}}\cdot \mathbf{v} \operatorname{d}t & \mathrm{parameterize\ the\ path\ with\ time} \\
 \int \mathbf{F}\cdot \operatorname{d}\mathbf{x} & = m \int \dot{\mathbf{v}}\cdot \mathbf{v}\operatorname{d} t & \mathrm{apply\ identity\ } \ddot{\mathbf{x}} = \dot{\mathbf{v}}\\
  \int_{t_0}^{t_f} \mathbf{F}\cdot \operatorname{d}\mathbf{x} & = \frac{m}{2} \int_{t_0}^{t_f} \frac{\operatorname{d} (\mathbf{v}\cdot\mathbf{v})}{\operatorname{d} t} \operatorname{d} t  & \mathrm{chain\ rule\ backwards}\\
\int_{t_0}^{t_f} \mathbf{F}\cdot \operatorname{d}\mathbf{x} & = \frac{m}{2} \left[\mathbf{v}\cdot\mathbf{v} \right]_{t=t_0}^{t_f} & \mathrm{fundamental\ theorem\ of\ calculus}
\end{align}
Note that in the "parameterize the path with time" step that whenever you do a path integral you have to parameterize the path somehow, and the result is independent of the parameterization chosen. So, we chose a convenient parameterization for our purposes.
It's possible to do the proof without using Leibniz's notation at all, but it's more cumbersome. Note that nowhere did I "cancel differentials".
A: What you are missing is the change of variable $s\mapsto s(t)$:
$$\int_0^l a(s)ds = \int_0^T a(s(t))\dot{s}(t)dt$$
where I prefer to use dots for the differentiation with respect to time as this is more classic a notation in physics. And $s(T)=l$. From there, this is trivial as $a(s(t))$ is the acceleration at time $t$, and it is therefore equal to $\dot{v}(t)$ where $v(t)$ is the speed at time $t$, which is also equal to $\dot{s}(t)$ as you noticed, so
$$\int_0^l a(s)ds = \int_0^T \dot{v}(t)v(t)dt=\int_0^T \dot{E}_c(t)dt=E_c(T)-E_c(0)$$
where, of course,
$$E_c(t) = \frac{1}{2}v(t)^2.$$
I had assumed you implicitly postulated a motion on a straight line but seeing Sean's answer, I feel like pointing out that my answer would be correct for a curved path as long as $a$ is the tangential acceleration!
A: A proof could go as follows:
Let $\Omega \in\mathbb{R^3}$, and consider the force field (which is a vector field) $\textbf F:\Omega \rightarrow \mathbb{R^3} $. Now, consider a particle $P$, of mass $m$, and let $\gamma:[t_1,t_2]\rightarrow \Omega$, with $\gamma \in C^2([t_1,t_2])$ be the curve representing the path that $P$ follows in space. We assume that $\textbf F$ is the total force acting on P 
(Remember that the symbol $\cdot$ indicates the scalar product)
The work done by $F$ on $P$ between the instants  $t_1,t_2$, is defined as the line integral of $F$ over $\gamma$; that is, 
$$W=\int_\gamma \textbf F=\int_{t_1}^{t_2} \textbf F(\gamma(t))\cdot\gamma'(t)dt
 $$
By the second law, $\textbf F(\gamma(t))=m\textbf a(t)=m\gamma''(t)$, thus, if $\textbf v(t)=\gamma'(t)$ is the velocity of $P$,
$$
\int_{t_1}^{t_2} \textbf F(\gamma(t))\cdot\gamma'(t)dt=\int_{t_1}^{t_2}m\gamma''(t)\cdot \gamma'(t)=\int_{t_1}^{t_2}m\textbf v'(t)\cdot \textbf v(t)
$$
It's clear that $\textbf v(t)$ is a vector, hence we'll write it in terms of its coordinates: $\textbf v(t)=(v_x(t),v_y(t),v_z(t))$, and of course its derivative, the acceleration, can be written as  $\textbf v'(t)=(v'_x(t),v'_y(t),v'_z(t))$ . Hence, the scalar product between the velocity and the acceleration is $v_x(t)v'_x(t)+v_y(t)v'_y(t)+v_z(t)v'_z(t)$. Thus,
$$\int_{t_1}^{t_2}m\textbf v'(t)\cdot \textbf v(t)=m\int_{t_1}^{t_2}(v'_x(t),v'_y(t),v'_z(t))\cdot (v_x(t),v_y(t),v_z(t))=m\int_{t_1}^{t_2}(v_x(t)v'_x(t)+v_y(t)v'_y(t)+v_z(t)v'_z(t))dt=m\int_{t_1}^{t_2} v_x(t)v'_x(t)dt+ m\int_{t_1}^{t_2} v_y(t)v'_y(t)dt+m\int_{t_1}^{t_2}v_z(t)v'_z(t)dt  $$. 
Now it's easy to see (if not, just integrate by parts) that $\int_{t_1}^{t_2} v_x(t)v'_x(t)dt=\frac{1}{2}(v_x^2(t_2)-v_x^2(t_1))$, and the same for the other two integrals. Therefore, we have
$$ W=\frac{1}{2}mv_x^2(t_2)+\frac{1}{2}mv_y^2(t_2)+\frac{1}{2}mv_z^2(t_2)-(\frac{1}{2}mv_x^2(t_1)+\frac{1}{2}mv_y^2(t_1)+\frac{1}{2}mv_z^2(t_1))=\frac{1}{2}m||\textbf v(t_2)||^2-\frac{1}{2}||\textbf v(t_1)||^2  $$, if we remember that $a^2+b^2+c^2$ is the length of the vector $(a,b,c)$.
A: I prefer to think of it without any reference to integration at all. One defines the power exerted by a force as $P_i = \vec F_i \cdot \vec v.$ When one sums up all of these powers exerted, one sees that $$\sum_i P_i = \sum_i \left(\vec F_i \cdot \vec v\right) = \left(\sum_i\vec F_i\right)\cdot\vec v = m \frac{d\vec v}{dt} \cdot \vec v,$$where we recognize Newton's second law as well as the distributive law for the vector dot product.
Now the product rule tells us plainly that if the mass does not change, $$\frac{d}{dt} \left(m \vec v \cdot \vec v\right) = m~\frac{d\vec v}{dt} \cdot \vec v + m~\vec v\cdot\frac{d\vec v}{dt} = 2 m~\frac{d\vec v}{dt} \cdot \vec v.$$Moving the factor of $2$ into the leftmost parentheses we find the rest of the rightmost side is equal to what we had above and this forces$$\sum_i P_i = \frac d{dt}\left(\frac12 m \vec v\cdot\vec v\right) = \frac{dK}{dt},$$ where the kinetic energy $K = \frac12 m \vec v\cdot\vec v.$ This is the differential form of the work-energy theorem. 
Of course if you wish to connect this back to actual work, then you will need an integral. Define the work as $W_i = \int_{t_0}^{t_1} dt~P_i$ over some time interval, and then observe that $$\sum_i W_i = \int_{t_0}^{t_1} dt~\left(\sum_i P_i\right) = \int_{t_0}^{t_1}dt~\frac{dK}{dt} = K_1 - K_0$$directly, because integration is a linear operation.
