Functional Programming, Formal Methods.
(Note that I used a Curry-Style rather than a Church-Style here, because that’s how Aaron’s proposal is presented. It isn’t clear how to present Self types with Church-style. Also, for simplicity, I ignored distinctions regarding explicit/implicit products.) The core of the idea is simple: by