2) it's a pretty rare skillet with specialist tooling, that doesn't really provide the itch scratch of most open source
3) "correctly formulating the problem in a formal specification" is really hard, given the inability of most stack overflow posters to formulate questions rigorously
4) for almost all projects, we value mutability over eternity
a lot of software is deployed in the service of the goals of business. To serve that purpose it often isn't necessary for the software to be completely correct. If it is probably sort of correct that's often good enough. Better to have something sort of correct deployed and running next week than something that costs more money and time to build, is a lot harder to hire people to maintain, relies on a formal analysis that is highly sensitive to changes in assumptions, and achieves a level of correctness that is unnecessary for the situation.
from this perspective, investing effort into formal methods will often give a poor return on investment compared to alternatives of hacking things together & running a few tests to catch obvious defects.
In some situations it seems to be worth investing in formal methods. Eg relatively well defined systems with very high costs if they fail.
Problems like that would go away with something like this, no? (if it is possible and there isn't a fault in my argument)
Did you? It seems pretty obvious to me that Rockstar knew that this was slow as hell, and they were showing ads during that time window. Business interests are not software engineering interests, so I don't think problems like that would go away with something like this, no.
So all this will really do is put more load on their servers, now that the bottleneck moved off of your hardware and back onto thiers.