Coding vs. Specifying Optimization tasks

Since many synthesis systems will have unique internal representations, there should be a way to manufacture conventional optimizers easily.

Program specification is about defining what a program will do. Since, given a specification, one can simply try enumerate-and-test, program synthesis is only about optimization. For scale purposes, conventional optimizers seem necessary, but building them by hand is expensive. Much of the code in an optimizer consists of routines that interpret how information flows across various syntactic constructs.

While this can be encoded by hand, we found that as Sinapse's internal form evolved and grew in complexity, the optimizer had to evolve in lock step. We often wished that we could instead specify something like the denotational semantics [#!Pagan81a:formal-spec-primer!#], and ``compile'' that into practical optimizers. In essence, we need an optimizer generator. Basic research is needed to accomplish this task.

Another possibility is for the synthesis community to agree on a widely usable internal form. This would allow tools to be made generically available. We believe this avenue is unlikely because a long search for UNCOL has largely been unsuccessful, and we expect that the utility of internal forms will come from their domain specificity.