You have to see it from janestreet's perspective. They're an HFT and trading high volume (millions if not 10's of millions) of stock & instruments. There is no "fix". By the time you understand what's wrong you've lost billions.

So yeah - offensive may work in non-critical areas.

Fwiw - you already use defensive everywhere. Python, Java, etc. come with garbage collectors. It's verified that the code is executing your intent.

I was wondering when we would start seeing formal verification. It makes sense that we would go from worrying about implementation details to a scientific/mathematical description of the problems.