Completely unambiguous. Completely intractable?
Here's an unambiguous program specification:
Write a program which takes as input a list whose elements all have the same type and a total order on the elements of the type. This program should output a list for which all of the following hold:
1) Every element of the appropriate type must occur exactly as many times in the output list as it does in the input list. (Zero is a perfectly good number.)
2) If an element in the input list is less than another element according to the total order, the lesser element must appear first in the output list.
3) If an element in the input list is not less than another and if it occurs after the other in the input list, it must occur after the other in the output list.
Put differently, write a stable sort. Even though there are multiple stable sorting algorithms, this specification is not ambiguous--for every input list and every valid total order, there is exactly one possible output list. I have precisely specified the effect of a stable sort.
Can a stable sort be derived? In theory, a sufficiently clever algorithm could deduce insertion sort. Herein lies the rub. A algorithm which can derive any program from its specification or fail if it doesn't exist is a general theorem prover, and it turns out that those are really hard to write. However, it also turns out that theorem checkers are much easier to write, and tests are even easier. Hence the strength of testing tools, the weakness of type systems, and the abject failure of business rules engines.
Functional programmers like to say that their languages let them declare what the program does instead of how it does it. That isn't really true; we're still writing the How, just at a higher level. Really, I can only think of one general purpose tool which can make the leap from What to How. Your brain.