The issue with formal proofs is that we might end up with correct code that does the wrong thing. I mean, something that the market doesn't care about. At the same time a buggy set of PHP scripts does what people care about and captures the market. Think about 20+ years ago and you find a lot of examples.
Well, sure — and the issue with tests is we might end up with well-tested code that does the wrong thing.
https://xkcd.com/224/ lol
Zuckerberg became rich on php, which grinds my gears almost as much as the genocide thing.
In fairness, my peers at $corp used to ship while I was sad-Wojciech "no you can't create tech debt". The universe is cruel to people who care.