This is a nice post! Jeremy Siek wrote a similar post a few years ago:

http://siek.blogspot.co.uk/2012/07/crash-course-on-notation-...

If I could add one thing to these two posts, it would be to learn Prolog.

We write inference rules top-down ("from these premises, we draw this conclusion"), but we often read them bottom-up ("given this goal, what facts could have lead to it?").

This double-vision thing, where you simultaneously view a set of inference rules in both a deductive and goal-directed fashion, is IMO one of the main stumbling blocks for people new to type theory. Luckily[1], however, it's fundamentally the same intuition that Prolog programmers develop -- and learning new programming languages is usually easy for programmers.

[1] It's not really by luck, of course: Prolog is called a logic programming language for a reason...