Well if you look at the categorical semantics of differentiation, it takes in a function A -> B and spits out AxA -> B. It’s a fairly well developed area of log

Well if you look at the categorical semantics of differentiation, it takes in a function A -> B and spits out AxA -> B. It’s a fairly well developed area of logic/type theory (even at the level of term rewriting systems), it seems the author of the blog post missed it. I probably would have emailed him some references if I’d seen the initial announcement...