Let $k$ be a ring and $\overline{k} = k[\epsilon]/\epsilon^2$. For every $f \in k[t]$ there is a unique $f' \in k[t]$ such that $f(t+\epsilon)=f(t)+\epsilon f'(t)$ holds in $\overline{k}[t]$. It follows that $f \mapsto f'$ is a derivation. For example, the leibniz rule:

$(fg)(t+\epsilon)=f(t+\epsilon) g(t+\epsilon)=(f(t)+\epsilon f'(t)) (g(t)+\epsilon g'(t))$ $=f(t) g(t) + \epsilon (f'(t) g(t) + f(t) g'(t)) + \epsilon^2 f'(t) g'(t) = (fg)(t) + \epsilon (f'(t) g(t) + f(t) g'(t))$

Now what about the chain rule $(f \circ g)'(t)=g'(t) f'(g(t))$? Is there a proof for this just using the definition above? Of course, you could argue that it suffices to take $f=x^n$ and then use inductively the leibniz rule. Or you recoqnize $f'$ as the usual formal derivative of $f$ and make an explicit calculation. But I wonder if there is a direct proof in the sense that you just use the definition of $f'$ above. Perhaps this then makes sense in more general situations as well.