Surprisingly, there is an interesting proof-theoretic connection between differential and sequent calculus! For a more detailed account of differential linear logic (DiLL), see Erhard [1] and Kerjean [2].

More generally, the same rules from differential calculus have reappeared in strange and marvelous places throughout computer science, including formal language theory [3], parsing [4], type theory [5] and automata theory [6].

We do not attempt to cover all these topics, research is just beginning to understand how they are related. The general theme seems to be, how do you propagate local changes through a computation? Can you compute changes incrementally without restarting from scratch?

[1]: https://arxiv.org/pdf/1606.01642.pdf

[2]: https://lipn.univ-paris13.fr/~kerjean/papers/EDP18.pdf

[3]: https://en.wikipedia.org/wiki/Brzozowski_derivative

[4]: https://dl.acm.org/doi/10.1145/2034773.2034801

[5]: http://strictlypositive.org/diff.pdf

[6]: https://en.wikipedia.org/wiki/Boolean_differential_calculus