The introduction and chapter 1 of the (free) homotopy type theory book (<a href="http:&#x2F;&#x2F;homotopytypetheory.org&#x2F;book&#x2F;" rel="nofollow">http:&#x2F;&#x2F;homotopytypetheory.org&#x2F;book&#x2F;</a>) 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.<p>Many of us are probably only exposed to type systems through, say, Java.  This is unfortunate because Java&#x27;s type system is rather primitive, and limits one&#x27;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.<p>*=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.