A notable exception is Scala's type system, which is pretty expressive. It has been formalized and proven to be sound[0].

[0]: http://scala-lang.org/blog/2016/02/03/essence-of-scala.html