How to take the derivative of a computer program

We will show how to differentiate computer programs (lambda-expressions, Turing machines, etc) by encoding them in a new system called linear logic that endows the space of programs/proofs with the structure of a differential k-algebra. We will discuss this theory from the perspective of the Curry–Howard–Lambek correspondence and discuss its semantics. Then formally, any program can be synthesized by gradient descent on the derivative of the universal Turing machine.