> So for example today I dealt with a synchronization issue. This turned out to not be a code bug but a human misunderstanding of a protocol specification saga, which was not possible to code into a type system of any sort.

Maybe not in a reasonable language no, but there are advances in type systems that are making ever larger classes of behaviours encodable into types. For example, algebraic effects (can this function throw, call a remote service etc)

https://koka-lang.github.io/koka/doc/index.html

linear types (this method must be called only once etc)

https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/line...

dependent typing (f(1) returning a different type from f(2), verifiable at compile time),

https://fstar-lang.org/index.html

Some of these features will eventually make it to “normal” PL. For example, Scala now has dependent types,

https://dotty.epfl.ch/docs/reference/new-types/match-types.h...

and Java can support linear type checking,

https://checkerframework.org/manual/#must-call-checker