All type systems will have meaningful and true propositions which are apparent to the programmer but not yet to the language team. Choosing a typed language is choosing to have a relationship with a living & evolving team/ecosystem, one which can improve over time in their ability to express and prove propositions or provide ergonomic abstractions.

Some of what the author is complaining about matches my conversations with people who aspire to be Rust library authors — that you're often trying to hijack the type system because you <do> actually know better.