Experimentation with techniques for deductive program synthesis is limited by the complexity of the necessary analysis, transformation, and search infrastructure. Prior to any experimentation with new ideas to perform code transformation and search, a substantial amount of foundational infrastructure must be created. The poco language is a small extension to the MinCaml subset of Ocaml that adds constructs for specifying code transformations, constraints guiding their application, and strategies for composing them. Its purpose was to serve as this foundational infrastructure for exploring ideas in synthesis methods before applying them to more complex languages. The poco implementation is designed to support backtracking search for enumeration of programs derived from a specification, with static analysis and pattern matching algorithms designed to reduce unnecessary computation wherever possible. This research presentation will detail the notable design decisions in poco, their impact on performance as measured through experimentation, and the use of poco to explore synthesis of algorithms guided by theorems from linear algebra.
poco: An ML testbed for deductive synthesis tool design (ml2020-paper81.pdf)