> For [Dependency resolution] and [Type checking], the worst-case just doesn't occur. ... at least in my career, I've never seen a galactic blow-up.
Both of these problems have been hand crafted and sanded down so as not to get into situations where there's exponential blow up.
> [Scheduling] and [Traveling Salesman] are technically optimization problems. Everyone knows you can tackle those with heuristics, ... We absolutely have tools that can find provably optimal solutions in reasonable time. There's no magic. No quantum computers. Just thinking harder and coming up with better algorithms. ... algorithmic speedup has outpaced hardware gains in the last decades. ...
The tools that can "absolutely find optimal solutions" don't, for even toy problems. Thinking harder helps, sometimes, but barely scratches the surface of most of these problems. Most of the time, thinking harder doesn't magically solve these problems.
> Last but not least: even (5), the archetype of NP-hard problems, is routinely solved at scale.
If this were even remotely true we'd have seen substantial progress in automated theorem proving well before the last couple of years. Notice how there are many math problems succumbing to automated techniques? This isn't because SAT solvers "routinely solve this at scale", it's because LLMs are getting better.
Why do we need type checking in the first place? One reason is to help find bugs. We need to enforce type checking to reduce bugs because reducing programs to SAT to ensure they're bug free is intractable. SAT is solved at scale? Why haven't they made solvers to prove your code is bug free so you don't need type checking in the first place?
I'm not up on scheduling software or research but my bet is that people who actually write schedulers would say that those tools that "absolutely" solve the problem absolutely don't.
The post almost gets it but never quite makes the leap. Taking Turing machines, for example. It's pretty easy to show that the Halting problem is undecidable. It doesn't mean all programs can't be analyzed, it means that there's no general method that will work for all programs. We don't give up on writing programs, we restrict ourselves to programs that we can reason about.
The ensemble, the space of problems we draw from, is specifically chosen so that we can do interesting work. But even that's restrictive and we're trying to constantly push to see what other programs we can analyze that are past our current front of knowledge.
This reads like child going into a supermarket and declaring farming, logistics and food scarcity to be solved because of the abundant availability of goods on the shelf. The world we've made is specifically crafted so that normal use is smooth. The fact you can't see it means you're living in a coddled domain and haven't pushed past it.