Damiano Mazza (LIPN) and Michele Pagani (IRIF) will present at POPL 2021 the first proof of the almost everywhere correctness of automatic differentiation in the context of a higher-order, Turing-complete programming language.