> It would be great if every app could have formally verified code etc.—but the reason they don't has to do with businesses funding these projects, not with the engineers working on them.
You can look at it from the company's point of view: Net profit would go down if they formally validated everything. Put that way, it sounds horribly selfish of the business. But you could also look at it from society's view: Net value to society would go down if everything was formally validated. Why? Because much less software would be created. And, for something like a chat app, we (society) don't actually need the level of reliability that we'd get from formal verification. Don't waste the effort doing it, because it's a net loss. Go spend the time building something else.
The result is that we get chat apps that crash. But we also get much more total stuff. I think that's a net win, even though it's annoying when the chat app crashes.
You can look at it from the company's point of view: Net profit would go down if they formally validated everything. Put that way, it sounds horribly selfish of the business. But you could also look at it from society's view: Net value to society would go down if everything was formally validated. Why? Because much less software would be created. And, for something like a chat app, we (society) don't actually need the level of reliability that we'd get from formal verification. Don't waste the effort doing it, because it's a net loss. Go spend the time building something else.
The result is that we get chat apps that crash. But we also get much more total stuff. I think that's a net win, even though it's annoying when the chat app crashes.