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

Example

Footnotes:

Author: expye(Zihao Ye)

Email: git@localhost

Date: 2022-02-28 Mon 00:00

Last modified: 2022-09-23 Fri 00:04

Licensed under CC BY-NC 4.0