The libraries people write to prevent bugs like these from happening (at a low level, in the "keep metacharacters out of the command line" sense, not in the "don't accidentally put a conditional in the wrong place" sense which is the proximate cause of this bug) work in most languages, probably even C. By way of example: Ruby has a solid command line wrapping gem.

I think "you could use type checking to break that logic bug" shares a lot of structure as an argument to "the key to security is input validation". It's true-ish at a superficial level but almost totally useless in practice, because it depends on foreseeing what the exploitable bugs will be. If your proposed defense relies on a catalog of possible bugs, it's not a real defense.

Solid, ambitious type systems are a good thing. For other reasons.

Decomposing logic using Hoare triplets and properly incorporating assertions as hints to a model checker wouldn't significantly add time to the development process. There is a lot of misinformation about the supposed overhead of formal methods or the assumption that they must be total. A lot of this is due to the fact that formal methods are typically used in projects where serious harm or death could result from an error, and thus, the cost of verifying the project must exceed the potential risk for failure. An incremental approach is pragmatic and yields results. It does not require the totality of classical formal methods projects.

I have not noticed a significant increase in time for my own development efforts while incorporating model checking into my own software development process. That's anecdotal, but up until the past 10 years, there haven't been many OSS model checkers to choose from. In turn, the cost for using these tools have made it harder to have peer reviewed cost analysis. If using a commercial tool, it's because you were required to do so via FAA or similar. Hence, the adoption curve hasn't yet been wide enough to have the wide adoption you've alluded to. With both the availability of these tools and the increased tool-assisted nature of red team analysis, it'll come.

Language can't fix these problems alone. Not even Rust is a silver bullet here. But, the incorporation of formal methods is an additional layer in a good defense-in-depth strategy.