The introduction and chapter 1 of the (free) homotopy type theory book (http://homotopytypetheory.org/book/ http://homotopytypetheory.org/book/) provide a great

The introduction and chapter 1 of the (free) homotopy type theory book (http://homotopytypetheory.org/book/ http://homotopytypetheory.org/book/) provide a great overview of type theory and the Curry-Howard correspondence which, for me, was the moment when I developed a deep appreciation for (non-broken) type systems. Many of us are probably only exposed to type systems through, say, Java. This is unfortunate because Java's type system is rather primitive, and limits one's ability to take full advantage of Curry-Howard. Scala provides a good environment for developing some introductory experience with type-level programming, since it is sort of halfway* between Java and a dependently-typed programming language like Idris. *=Scala has higher-kinded types, path-dependent types (weaker than dependent types, but allows you to see what all the fuss is about), existential types, and implicit arguments - many of the ingredients that you will find in many theorem provers and proof assistants which, interestingly, rely on type theory (via Curry-Howard). Java has none of those.