Autodiff isn't even the most impressive application of non standard interpretation. The most impressive one is sparsity detection. If you have some arbitrary code that returns a matrix you can infer which elements of the matrix are guaranteed to be zero independent of input using non standard interpretation by taking all the branches of the program.

This discovered sparsity can be exploited by a lot the generic algorithms in Julia that also are able to efficiently work on sparse matrices. There is also a way of combining this with AD to get automatic sparse hessian of optimization which is huge.