On this page:
1.1 Installing Rosette
1.2 Interacting with Rosette
1.3 Rosette Dialects

1 Getting Started

Rosette is a solver-aided programming system with two components:

The name "Rosette" refers both to the language and the whole system.

1.1 Installing Rosette

To install Rosette, you will need to

1.2 Interacting with Rosette

You can interact with Rosette programs just as you would with Racket programs: either through the DrRacket IDE or through the racket command-line interpreter. We suggest that you use DrRacket, especially at the beginning.

Example Rosette programs can be found in the rosette/sdsl folder. Most of these are implemented in solver-aided domain-specific languages (SDSLs) that are embedded in the Rosette language. To interact with an example program, open it in DrRacket and hit Run!

1.3 Rosette Dialects

The Rosette system ships with two dialects of the Rosette language:

To use the safe dialect, start your programs with the following line:

#lang rosette/safe

To use the unsafe dialect, type this line instead:

#lang rosette

We strongly recommend that you start with the safe dialect, which includes a core subset of Racket. The unsafe dialect includes all of Racket, but unless you understand and observe the restrictions on using non-core features, your seemingly correct programs may crash or produce unexpected results.