[chriswarbo]

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!)

[dvt]

> 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.

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).