UCSD does a lot of cool type system stuff. Also check out Liquid Haskell (another UCSD project), a refinement type system added to Haskell. A good book to read

UCSD does a lot of cool type system stuff. Also check out Liquid Haskell (another UCSD project), a refinement type system added to Haskell. A good book to read to learn more about the crazy things you can do with a dependent type system is the Idris O'reilly book as well. If you're like me and think modern software practices are scarily inadequate at proving correctness, but you still need high performance, take a look at Rust. It also has a very nice type system with ADTs, and it's being improved all the time. Unlike Haskell and Idris, it's not geared towards research and has no GC, so it has near C/C++ performance.