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

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, seemingly correct programs may crash or produce unexpected results.