I think our options basically come down to types, tests, and syntax. Syntax is the least explored because it's expensive to iterate on and teams can't agree on

I think our options basically come down to types, tests, and syntax. Syntax is the least explored because it's expensive to iterate on and teams can't agree on it, so we sit around hoping that the next generation of languages will let us consume a better syntax instead of daring to build one. But a syntactical approach leads towards writing the specification in terms of the high level description, folding up lower level pieces of the problem into bits of syntax, and then having them meet in the middle with "enough" compilation. You end up with a program that is right because it literally can't be written wrong. Types do some specification, but they work in a more bureaucratic sense of "you have to do what you mean" by checking to see if you filled out the right form. Of course teams love doing that, because they need a little bit of bureaucracy. Everyone seems to agree on some amount of type discipline being needed at scale. Tests exist at the far end of specification, where the program is just "what it's been tested to be." This is most useful when you don't have a clear specification and you're mostly looking at the integration side of things, not deeply examining the behavior. Teams can add lots of tests, but the tests are a scattershot and don't always do anything specific. They do have a tendency to tell you how a change will break an existing specification, though.