I have mixed feelings about this. I've been through nonstandard analysis. My response was, "We shouldn't need the axiom of choice to define the derivative."

But I think that it is extremely important to understand that the infinitesimal notation really MEANS something. Here is some Python to demonstrate.

    # d is a functor. It takes a function and returns a second function.
    # The second function captures the change in f over a small distance.
    # The dx/2 business reduces artefacts of it being a finite distance.
    def d (f, dx=0.001):
        return lambda t: (f(t + dx/2) - f(t - dx/2))

    # d²x / dx²
    def second_derivative (f):
        return lambda t: d(d(f))(t) / (d(x)(t) * d(x)(t))

    def x (t):
        return t

    def cubed (t):
        return t*t*t

    print("The second derivative of cubed at 1 is near", second_derivative(cubed)(1))