jputnam (jputnam) wrote,

Completely unambiguous. Completely intractable?

Reddit recently linked to a speech by Joel Spolsky containing an often-stated saw, namely that a completely unambiguous program specification can be automatically transformed into a working program. In other words, once the specification is written, there is nothing else for a programmer to do. I used to accept this statement at face value. I was wrong.

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.
  • Post a new comment

    Error

    default userpic

    Your reply will be screened

    Your IP address will be recorded  

  • 3 comments