Okay, then let me define a new axis: useful vs. useless type systems. A type system is useful to the extent types rule out implementation errors and/or miscommu

Okay, then let me define a new axis: useful vs. useless type systems. A type system is useful to the extent types rule out implementation errors and/or miscommunication between the implementer and the user of an abstraction: (0) Algebraic data types, pattern matching and exhaustiveness checking rule out forgetting to handle all the qualitatively different possible outcomes of an operation. (1) Statically typed effects rule out sneaking effects into computations without making them knowable to the user. (2) Substructural type systems rule out resource leaks and uses after free. (3) Rust's borrow checker rules out concurrent modifications of the same object in memory. How usefully typed are C and Java?