rosette-lang is an actively used programming language created in 2013. 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.
- the rosette-lang website
- rosette-lang first appeared in 2013
- rosette-lang was created by Emina Torlak and Rastislav Bodik
- Have a question about rosette-lang not answered here? Email me and let me know how I can help.
Example code from the web:
#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)))
Last updated August 9th, 2020