Differentiation lies at the core of many machine-learning algorithms, and is\nwell-supported by popular autodiff systems, such as TensorFlow and PyTorch.\nOriginally, these systems have been developed to compute derivatives of\ndifferentiable functions, but in practice, they are commonly applied to\nfunctions with non-differentiabilities. For instance, neural networks using\nReLU define non-differentiable functions in general, but the gradients of\nlosses involving those functions are computed using autodiff systems in\npractice. This status quo raises a natural question: are autodiff systems\ncorrect in any formal sense when they are applied to such non-differentiable\nfunctions? In this paper, we provide a positive answer to this question. Using\ncounterexamples, we first point out flaws in often-used informal arguments,\nsuch as: non-differentiabilities arising in deep learning do not cause any\nissues because they form a measure-zero set. We then investigate a class of\nfunctions, called PAP functions, that includes nearly all (possibly\nnon-differentiable) functions in deep learning nowadays. For these PAP\nfunctions, we propose a new type of derivatives, called intensional\nderivatives, and prove that these derivatives always exist and coincide with\nstandard derivatives for almost all inputs. We also show that these intensional\nderivatives are what most autodiff systems compute or try to compute\nessentially. In this way, we formally establish the correctness of autodiff\nsystems applied to non-differentiable functions.\n