[vog]

Note that proper typesystems are not yet mainstream, though.

You should certainly have a look at "less mainstream" languages whose type systems are more expressive and still simpler to use than those of the "mainstream" languages. For example (list is incomplete, but you'll get the idea):

    * Haskell (very popular, hard to reason about performance, though)
    * OCaml (possible to reason about performance, except for garbage collection)
    * Idris (type system with dependent types!)
    * Rust (type system that allows to reason about memory usage, aliasing, etc.)
    * Elm (meant to replace JavaScript for user interfaces in the browser)

[rtpg]

I would add Purescript to that list. Most people see it as a Haskell-like for the JS VM, but it also includes row types. Meaning that your types can keep track of granular effects ("oh, this uses IO, but just the random number generator", "Oh this just looks at the foo property"), which is super useful for reasoning with larger codebases.

[lomnakkus]

Agreed. Purescript[1] is definitely interesting as one the very few languages in the world with row types/polymorphism.

I'm not quite agreed on the effects bit being useful, but it's a good demo of what the type system can do. My main disagreement with the whole approach is that effects don't commute (in general) and so representing effects as such isn't quite valid.

[1] I'm still baffled as to why they named it thusly. I mean, I can guess at motivations, but it really deserves a much catchier name!