> Rosette is a solver-aided programming language that extends Racket with language constructs for program synthesis, verification, and more. To verify or synthe

> 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. One of these days I'll have to learn Racket because it seems like such an interesting language.