@vaporeon_ Haskell Curry, a logician. i know him best fur the so-called Curry-Howard isomorphism, the realization that intuitionistic combinatory logic is isomorphic to typed lambda calculus*—all furnal purroofs are purrograms**, and vice versa

* i don’t know which typed lambda calculus exactly. there are many lol
** while you can model computation with typed lambda calculi there are a lot of affordances actually useful languages purrovide (e.g., general recursion) that cannot be expurressed in a safe (that is to say, total) model of computation