Sometimes you still are required to solve them as far as you can. The problems solved by systems like TLA+ or ACL2 can also be useful, and those are both free t

Sometimes you still are required to solve them as far as you can. The problems solved by systems like TLA+ or ACL2 can also be useful, and those are both free tools (ignoring engineer time). The absolute cost of solving a problem isn't the best measure for how "big" it is. It's a good reminder though in reference to the GP that there's a richness in methods beyond what one might expect a programming language by itself to handle -- can you imagine someone proclaiming "I can't understand how people use languages without [input from my multi-million dollar] static analysis [tool]."?