The smooth infinitesimal analysis assumption that all functions are infinitely differentiable indeed removes a lot of edge cases, but only in the way that the C

The smooth infinitesimal analysis assumption that all functions are infinitely differentiable indeed removes a lot of edge cases, but only in the way that the C assumption that all memory accesses are within bounds removes a lot of edge cases. Just as a C programmer may have difficulty telling a valid C program from a meaningless sequence of symbols, so does SIA make it difficult to tell a valid assumption from a paradoxical statement that would allow defining a non-differentiable function. If you have a correct calculation in SIA involving infinitesimals squaring to zero, it can easily be translated into the classical setting using functions that have their magnitude bounded above by a quadratic in a neighborhood of zero, but with the advantage that if you try it on a non-differentiable function, you'll merely fail to prove the quadratic upper bound instead of getting nonsensical results. Such a "quadratic bound" approach (in brief f'(x) exists if there exist a constant C and a neighborhood of zero where for all h in the neighborhood |f(x + h) - f(x) - f'(x)h| ≤ Ch²) could actually be adopted over the typical limit of (f(x + h) - f(x))/h without abandoning classical logic, but considering the difficulty of proving the bound for many functions of interest, it might not make much of a difference over just assuming differentiability either way.