[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> It is not the job of our programs to instruct the computer. > Rather, it is the job of the computer to execute our programs. > In the case of programming by example and related program synthesis technologies, it really is our job to instruct the computer. We provide it with an a possibly underdetermined set of functional constraints or inconsistent set of training examples. The computer's job is to find any one (of potentially many with equal scores) program, filling in the details, that best matches the request. I suppose one could argue that this isn't the activity of programming a computer -- it's the activity of using some software that let's you make queries against an implicitly defined database of possible structures that could later be treated as executable programs (or hardware designs in other applications). The physical machine is enacting some specific algorithm to search the space of potential outputs and filter them by the constraints, but details of this algorithm sink below the level of our perception in the same way the microcode in modern CPUs is invisible even to the assembly programmer. Whatever this activity, however, it is the hallmark of the programmer/modeler/domain-engineer's job when using a (programming) paradigm like answer set programming. We write documents in formal languages that we call programs programs, and we "run" them to get output with controllable properties that we expect. The implementers of the search software have conspired with the hardware to offer us the illusion of programming against an inherently nondeterministic machine in which nature finds a way such that we only observe it guessing valid solutions. Certainly, this is an illusion offered by abstraction levels, squinting, and convention, but so are all of the potential levels one might program at below it all the way down to the quantum level. In any nondeterminstic programming setting, it's the programmer's intent to enlist support of something outside of their own code (somewhere between a hardware random number generator and a SAT solver) to carry out some form of "filling in the details". Meanwhile, I'll agree that this phenomenon isn't too relevant when describing the nature of a C compiler (superoptimizing compilers written as nondeterministic programs aside).
