Hi everyone, tomorrow I'm going to be presenting Rosette and the Rosette paper at the
reading group. For some more context, Rosette is one the solved-aided languages I'm using to implement a SemGuS solver, since it has the capability of synthesizing symbolic constructs and ASTs.
Abstract:
SAT and SMT solvers have automated a spectrum of programming tasks, including program
synthesis, code checking, bug localization, program repair, and programming with oracles. In principle, we obtain all these benefits by translating the program (once) to a constraint system understood by the solver. In practice, however, compiling a language
to logical formulas is a tricky process, complicated by having to map the solution back to the program level and extend the language with new solver-aided constructs, such as symbolic holes used in synthesis. This paper introduces Rosette, a framework for
designing solver-aided languages. Rosette is realized as a solver-aided language embedded in Racket, from which it inherits extensive support for meta-programming. Our framework frees designers from having to compile their languages to constraints: new languages,
and their solver-aided constructs, are defined by shallow (library-based) or deep (interpreter-based) embedding in Rosette itself.
Homework question:
The author's course on solver-aided programming at CAV 2019 goes over a good example
of a circuit language SDSL with both deep and shallow embedding, which can be found here -
https://homes.cs.washington.edu/~emina/media/cav19-tutorial/lab2.html.
See if you can complete some of the verification & synthesis exercises for this topic,
as it is particularly relevant to what I'm doing with SemGuS, and I plan to go over it during the presentation.
Also, here is the actual paper link:
https://homes.cs.washington.edu/~emina/doc/rosette.onward13.pdf
![[Computer Systems Lab]](http://www.cs.wisc.edu/pics/csl_logo.gif){kind=logo}