|
I think different contexts call for different kinds of specification, but most commonly, I do think "synthesize a _function_ which for inputs x1, x2, ..., xk produces outputs y1, y2, ..., yk respectively", is a pretty good setup provided you then are willing to test it on xk+1 ... xn. The "programming-by-example" research direction aligned nicely with TDD, and functions provide a nice abstraction layer. I _don't_ think a detailed program trace is the best "specification" in most cases because constructing that log includes making a lot of choices of _how_ the program arrives at its outputs. The full trace for meaningful programs might be quite large, and onerous to specify (or you'd just produce one from an already-working program, in which case what's the point?). For me, the benefit of synthesis should be that the programmer can describe what should be done, rather than how. However, this can quickly lead to a complex "specification language" which can be just as burdensome to write in as the desired target language, which is why examples are appealing. But perhaps some combination, where we provide some examples and also some formally specified restrictions ("the `get_work_history` method returns `jobs: List[Jobs]` such that `map(_.start_date, jobs)` is non-decreasing according to the default comparator on Dates ...") is best, since examples will generally underspecify the program. Update: the 'different contexts' I think is mostly that sometimes, some specific attributes of 'how' the synthesized program accomplishes its goals do matter -- e.g. you may want to synthesize some mathematical optimization code which really ought to use the GPU, and that isn't indicated in just input/output examples, or you may want to ensure that part of an embedded system uses constant memory and returns after a constant number of steps. |