> The primary objective of a type system is to detect programming errors. The type system effectively provides a limited form of static verification, allowing us to express certain kinds of invariants about our code that the compiler can verify. Type systems provide other benefits too of course, but error checking is its Raison d’Être.

I'd argue that understandability should be the goal. Verification without understandability is a loss. Understandability without type-based verification can win. Put understandability first with types and get the benefit of both.