3 Syntactic Forms

The core of the Rosette language (rosette/safe) consists of two kinds of syntax forms: a set of basic forms lifted from Racket, and a set of forms for solver-aided programming. We use the term "lifted" to refer to parts of the Racket language that can be used with symbolic values and other solver-aided constructs.

    3.1 Lifted Racket Forms

    3.2 Solver-Aided Forms

      3.2.1 Symbolic Constants

      3.2.2 Assertions

      3.2.3 Angelic Execution

      3.2.4 Verification

      3.2.5 Synthesis

      3.2.6 Optimization

      3.2.7 Debugging

      3.2.8 Reasoning Precision