You are viewing jputnam

jputnam [userpic]

Completely unambiguous. Completely intractable?

December 4th, 2007 (01:10 am)

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.

Comments

Posted by: ((Anonymous))
Posted at: December 5th, 2007 10:48 am (UTC)
bad example

i think the example given is poor, because the wording of the specification is quite natural language oriented - if you had specified it in a more systematic syntax with predefined semantics, it would make parsing of the spec easy, and once the semantics of a spec is internalized, a program can be generated. but doesnt that sort of sound like...programming?

wot joel said was right - a fully spec'ed program is itself a program, just written in the language of the spec. getting that spec is where the real problem is in programming. a programmer is not just a code monkey, but someone who disambiguates an ambiguous spec.

Posted by: habitue01.wordpress.com (habitue01.wordpress.com)
Posted at: December 5th, 2007 11:11 am (UTC)
Re: bad example

No, his point is valid. He is saying that a specification can simply be a way to verify that a solution (i.e. program output) is correct. This is completely different from specifying how the program should arrive at the answer. Most theoretical computer scientists believe that finding a solution to a problem is a much harder proposition that verifying that a given solution is correct.

That is all a program spec has to do, tell how to verify correctness, the programmer has to come up with the implementation. For many things, it might be possible to have an automated way to come up with an implementation from the spec. For other things, there may be no efficient way for the computer to generate an implementation. As an example, try a spec that includes any NP-complete problem: Easy to verify correct, hard to come up with a correct solution.

Posted by: ((Anonymous))
Posted at: December 5th, 2007 01:14 pm (UTC)
Re: bad example

This isn't "wholy unambiguous" because it leaves a great deal of its terms undefined - it's relying on common knowledge and the interpretation of the reader to fill in the blanks. It's this second step that requires the intervention of a human (or strong AI).

3 Read Comments