Nice list. I have a new language I'm working on (called Zena: https://zena-lang.dev/) with all of these in some form:

If you have static types and unions, control-flow analysis and narrowing is critical for avoiding an excessive amount of casts - and if you also have pattern matching, you get very nice style where a type-check, state extraction, and branch are all one expression.

Borrow checking. Zena is a GC'ed language, but it runs in Wasm and lots of Wasm resources are external, so Zena has affine types and second-class values for managing resources and disposing of them when no longer used. GC + borrowing is a great combo because you don't need borrowing for everything and lexical lifetimes with a few escape hatches cover most things. The ownership system is also great for modeling structured concurrency.

I'm working on contracts after borrow checking is complete. My impetus there is AI-generated code. If humans still review at all, reviewing the contacts more than the implementations makes managing large amounts of changes easier.

I'd like to see a few more good ideas spread:

Formal verification. Contracts should be a good stepping stone into a spec language, from there a proof language and checker. This should also be good for AI-generated code.

Numeric unit types / units of measure with dimensional analysis. We should be able to say that a variable isn't just a f64, but a f64 of meters, and when divided by seconds, give a velocity. I don't know why this hasn't made it into more mainstream languages, but it seems like it makes programs more clear, not just statically safer. For synax, my plan is to parameterize scalars by units, like f64<m> vs f64<s> and have units like `m` and `s` be associated with dimensions like `length` and `duration`.

Async cancellation. I added cancellation as a first-class language concept in Zena so that it can be handled like exceptions, but aren't exceptions. It extends try/catch to try/catch/cancel/finally. When a task is canceled, a cancellation unwinds the stack starting from the next suspension point (await). The benefit here is that you don't have to remember to check for cancellation in async functions - they're all cancellable.