I disagree that converting from an equation to a solution algorithm is a straightforward process. It is very much where mathematics helps, for example just to e

I disagree that converting from an equation to a solution algorithm is a straightforward process. It is very much where mathematics helps, for example just to ensure convergence of the method. Also, the way you model reality (choose the equation) is often done with the limitations of solvability in mind. I also disagree that maths can help you pick the right equations, just like there is no formal method that can verify whether a program specification is appropriate to the problem. Equation (or a model) is just an infinite family of SAT problems, typically parametrized on our understanding what a "number" is. If we had a really good SAT solver, then getting a solution would indeed be a really straightforward process (just pick the number representation) of solving the instance. The same is also true for checking "legitimacy" (which I interpret as consistency) of the model - SAT solver would tell you that the instance is unsatisfiable and why. But you can never formally determine that the chosen SAT instance is appropriate model for the task at hand.