Explainable Program Synthesis by Localizing Specifications

Explore a groundbreaking approach to program synthesis in this 17-minute conference talk from OOPSLA2 2023. Delve into the concept of subspecifications as a mechanism to enhance synthesized implementations with explanatory notes. Learn how this novel method addresses the challenge of obscure correspondences between specifications, implementations, and user intent in traditional synthesis engines. Discover algorithms for constructing and verifying subspecifications, and examine their theoretical properties. Gain insights from an experimental evaluation of the subspecification generation procedure, assessing its effectiveness and performance. Understand the practical implications through a user study that demonstrates how subspecifications aid in comprehending global specifications, identifying alternative implementations, and debugging faulty code. Access supplementary materials, including reusable artifacts, to further explore this innovative research in explainable program synthesis.