Differential Programming Languages/Chapter-1-Syntactic-Differentiation

The derivative is often introduced as an operation on functions: given a function $f:ℝ\to ℝ$ it's derivative at a point $a$ is a linear function $D(f):ℝ\to ℝ$. In this book, the derivative is being developed as a programming language construct, so we will need to introduce the derivative as an operation programs $f:ℝ\to ℝ$. We will restrict our attention to functional programs which for our purposes will mean programs that represent mathematical functions. From this restriction, we can make sense of whether the derivative is implemented correctly -- i.e. that the differentiated program corresponds to the mathematical derivative of the function that the original program represents.

While this is not meant to be an enormous change, there are a few differences to point out:

1. The objects $ℝ$ are types in a programming language rather than sets.  Values in a set are always constructible, and we write $a:𝔸$ to denote that...

The immediate challenge is that a single mathematical function can be represented by syntactically different programs