Rosette: About (original) (raw)

Rosette is a solver-aided programming language that extendsRacket with language constructs for program synthesis, verification, and more. To verify or synthesize code, Rosette compiles it to logical constraints solved with off-the-shelf SMT solvers. By combining virtualized access to solvers with Racket’s metaprogramming, Rosette makes it easy to develop synthesis and verification tools for new languages. You simply write an interpreter for your language in Rosette, and you get the tools for free!

#lang rosette

(define (interpret formula)
  (match formula
    [`(∧ ,expr ...) (apply && (map interpret expr))]
    [`(∨ ,expr ...) (apply || (map interpret expr))]
    [`(¬ ,expr)     (! (interpret expr))]
    [lit            (constant lit boolean?)]))

; This implements a SAT solver.
(define (SAT formula)
  (solve (assert (interpret formula))))

(SAT `(∧ r o (∨ s e (¬ t)) t (¬ e)))

To learn more, take a look at The Rosette Guide,this talk,applications, courses, or publications.

Acknowledgments

This research was supported in part by awards from the National Science Foundation (NSF CCF 1651225, 1337415, 1139138, and 0916351), the Department of Energy (DOE DE-SC0005136 and DOE FOA-0000619), and gifts from Intel, Nokia, and Samsung. Rosette extends the Racketprogramming language, and uses the Z3 solver from Microsoft Research. Many thanks to the authors of these systems for making them freely available, and to Rosette users for many helpful comments and suggestions.