I agree that it seems like an extraordinarily difficult problem, but I don't find this particular dismissal convincing. It's much easier to reject something potentially unsafe than it is to generate something safe. That's the basis for all sound type systems and scales to extremely sophisticated types (e.g. it is fairly to define the type representing the Collatz Conjecture, and I think most people would agree that it is perhaps slightly more difficult to find an inhabitant of that type).

In this case, I don't even know if we're in the paradigm of "hard to satisfy types"--a lot of the time you can for example probably use an autobooking feature to get something you'd be okay with as a backup, but since you know it is suboptimal you still want to try to do better if possible. There are also plenty of real world control systems which perform fairly involved calculations, but still perform some basic sanity limits checks on the inputs and outputs to make sure that if the calculations screwed up, things don't fail catastrophically. In such cases the limits are much easier to define than a spec for how the whole thing works.