Thankfully this is no longer strictly true. So, I think the quote needs a slight adjustment, "Type systems and $THING are just ...", but $THING is not very well defined yet. Between "linters", and other relatively fast AST-based rule enforcers, some of which looking at higher order behavior, I think we now have an amalgamation of formally verified concepts that we can consider fast enough and sufficient exercised in practice that we are ever closer to widespread formally and dependably verified software.

Still, it's a long journey, and academic formal verification would always be, by design, a few steps ahead of what the industry can do efficiently in practice.

The field really needs more popularizers. I mean people or projects who can do "advertising" like, "if you add our linter to your CI/CD pipeline, you'll never have X class of bug ever again!"