A taste of Rosette and Program Synthesis
Table of Contents
Rosette is a program synthesis tool, first proposed in paper A Lightweight Symbolic Virtual Machine for Solver-Aided Host Languages by Torlak et al., recently my colleagues are using this tool to generate programs under certain constraints in our projets, which encourages me to study Rosette and related work on Program Synthesis.
What's Program Synthesis
When I first heard the term program synthesis, I think it was a synonym of Code Generation or compile. However this is not true, below is the definition of program synthesis from wikipedia1:
In computer science, program synthesis is the task to construct a program that provably satisfies a given high-level formal specification. In contrast to program verification, the program is to be constructed rather than given; however, both fields make use of formal proof techniques, and both comprise approaches of different degrees of automatization. In contrast to automatic programming techniques, specifications in program synthesis are usually non-algorithmic statements in an appropriate logical calculus