> We can't prove a program will always halt, but we can check it halts in a specific execution.
The computer scientist says “The halting problem cannot be solved, I have proven it” and the software engineer goes “30 second timeout, if the answer’s not ready by then we don’t need it”
I think this comparison is interesting because it shows the difference between theory & practice, but it's a little inaccurate. The halting problem being undecidable just implies there is no single universal algorithm that can tell you whether any program at all will halt. In practice we are working in specific domains and can come up with heuristics which are "good enough" for a specific codebase / module, like the timeouts you mention. So the halting problem can be solved for some subsets of programs but not all of them, and the computer scientist would hopefully have realized this instead of treating the codebase generically as "any program".