Languages Features Creators CSV Resources Challenges Add Language
GitHub icon


rosette-lang - Programming language

< >

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

#1610on PLDB 10Years Old 0Books

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
; A comment
Line Comments ;
; A comment
Semantic Indentation X
ook.html · rosette-lang.html · dcalgol.html

View source

- Build the next great programming language · Search · Day 213 · About · Blog · Acknowledgements · Traffic · Traffic Today · GitHub ·