I'm a big fan of giving more feedback to developers at compile-time. A while back I wrote a Java library that makes it easy to add static checks that would otherwise be runtime errors. Link in case someone finds it useful: https://github.com/overstock/annotation-constraints
The verification question is somewhat handwaved in the linked article, but in fact we are now in a position to verify some of this stuff mechanically. Unsurprisingly, the "branding" techniques work, but in type systems that have any amount of subtyping the argument for why they work is subtle and they may not work in all cases.
there are lots of properties app devs & library authors want to verify statically and languages aren't doing a good job of making this easy
JS (for example) has a bunch of 3rd-party type checkers (typescript, flow), and they're huge projects. And flow is even written in ocaml.
I've written static verification of non-type properties when my team absolutely needed it and it's never easy -- even things like AST walking can be rough and non-standard.
Would def try a language that had BYO static checks as a first-class concepts. Code generation is the closest thing to this IMO in widely used languages and even that is clunky in most places (go:generate, I'm looking at you).
Not really a language feature since it's compiler specific but you can relatively easily write static checks using clang-tidy which is a code analysis tool for C++.
Because we are lazy or overworked?
The last time I wrote C, I had asan and ubsan and valgrind running in CI.