Earlier quoted context omitted.
Any typing system that has at least two types (functional and non-functional) is a logic. In fact, modus ponens follows axiomatically via →elimination: Let α → H be a functional type where α is a Person type, and H is a boolean type. Γ ⊢ α → H Γ ⊢ α --------------------- (→e) Γ ⊢ H What this means is that you can have a function isAtHome(x) which takes a Person and returns a boolean. This schema itself is a logic ins…
Thanks, this is what I was getting at: the type systems of C++ and Java are logics in the sense of being formal syntactic systems with deduction rules. I was struggling to think of a concrete example less trivial than function application, but I suppose my difficulty just shows how terrible these systems are when viewed as logics (but they're still logics!)
Yep, exactly. Why I think it's hard to think of a more concrete example is because any type theory (like vanilla λ-calculus) is not deductive.
Let me clarify: once you add types to λ-calculus, it (amazingly) becomes deductive! But the type theory itself is not deductive (because types are not tractable, among other reasons).