Questions Columns Rows
GitHub icon

rosette-lang

rosette-lang - Programming language

< >

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

#1699on PLDB 10Years 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.


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

Language features

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

View source

- Build the next great programming language · Search · Add Language · Features · Creators · Resources · About · Blog · Acknowledgements · Stats · Sponsor · Traffic · Traffic Today · Day 278 · feedback@pldb.com · Logout