Yes, choosing the right criteria / spec to prove against is a big task, and one that is not done at all today. Mathematicians sometimes say that fully describin

Yes, choosing the right criteria / spec to prove against is a big task, and one that is not done at all today. Mathematicians sometimes say that fully describing the problem can be more work than actually proving it with a particular solution, and I imagine there's some parallels between that and the criteria vs proof problem you mention here. If there's a biggest problem it's that nobody cares about a good spec so nobody will pay for it.