Safe and Secure: Ada 2012 https://www.adacore.com/knowledge/technical-papers/safe-and-secure-software-an-invitation-to-ada-2012/ (criticises C, many other languages have adopted some ideas, but the subtyping is elegant)
miniblog.
Related Posts
I've really come to appreciate OCaml's notion of generics. It doesn't have subtyping, so e.g. you have an `int list` or an arbitrary `'a list`, but nothing inbetween.
As soon as you add constraints like Java's `List<? as Foo>` it become incredibly hard to produce good errors.
OCaml has several unusual design features that I've come to appreciate.
(1) Separating integer and float addition is really clear.
(2) No subtyping (everything is 'a or concrete) simplifies lots too.
Bidirectional type checking versus Hindley-Milner type checking, with some worked examples of subtyping: