This series of articles aims to explain why complicated type systems such as λC can be useful in practice, and how such use inevitably leads to the ability to formalize mathematics.
If you have been a software engineer and ever wondered "Why those PLT people invent all these fancy concepts about types?" This series might answer your question.
I will assume some very basic knowledge of major programming languages such as java, python, C, and notably haskell. If you have never used haskell, I strongly recommend that you try it. It can change your life. A good place to start is Learn You a Haskell for Great Good.