[9rx]

Coq, Idris, et. al. are over there if that's what you really want, but there is probably good reason why no "real world" programs are written in languages with proper type systems.

For one, there's little ability to avoid message passing in our modern world. You can take it out of the language, but that just means pushing it to another abstraction (e.g. sockets), and all the same lack of type safety comes right back.