rosette-lang

rosette-lang is a programming language created in 2013 by Emina Torlak and Rastislav Bodik.

#1703on PLDB

11Years Old

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.

rosette-lang website
rosette-lang first developed in University of California, Berkeley
Read more about rosette-lang on the web: 1.

Example 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)))

Feature	Supported	Token	Example
Comments	✓		; A comment
Line Comments	✓	;	; A comment
Semantic Indentation	X

rosette-lang - Programming language

Language features