The Rosette Language

Rosette is a solver-aided programming language that extends Racket 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, applications, or publications:

  • [1] Emina Torlak and Rastislav Bodik. A Lightweight Symbolic Virtual Machine for Solver-Aided Host Languages. PLDI 2014. (ACM, PDF)
  • [2] Emina Torlak and Rastislav Bodik. Growing Solver-Aided Languages with Rosette. Onward! 2013. (ACM, PDF)