  Formal transformations somehow resembling the usual derivative are
surprisingly common in computer science, with two notable examples being
derivatives of regular expressions and derivatives of types. A newcomer to this
list is the incremental $\lambda$-calculus, or ILC, a "theory of changes" that
deploys a formal apparatus allowing the automatic generation of efficient
update functions which perform incremental computation. The ILC is not only
defined, but given a formal machine-understandable definition---accompanied by
mechanically verifiable proofs of various properties, including in particular
correctness of various sorts. Here, we show how the ILC can be mutated into
propagating tangents, thus serving as a model of Forward Accumulation Mode
Automatic Differentiation. This mutation is done in several steps. These steps
can also be applied to the proofs, resulting in machine-checked proofs of the
correctness of this model of forward AD.
