What's great about its type system? I find it severely limited and not actually useful for conveying and checking invariants.