Solver-Aided Programming with Rosette | Schema Programming Part 33

This is the cutting edge. Rosette is a language built on Racket that integrates with SMT solvers (like Z3). It enables Solver-Aided Programming.

Symbolic Execution

In normal Racket, x is a specific number (like 5). In Rosette, x can be a symbolic integer—meaning it represents all possible integers at once.

#lang rosette

(define-symbolic a b integer?)

Verification: Finding Bugs

We can ask Rosette: "Is there any input that breaks my code?"

(define (safe-div x y)
  (if (= y 0) 0 (/ x y)))

; Verify that safe-div never crashes
(verify (assert (eq? (safe-div a b) (safe-div a b))))

Synthesis: Writing Code for You

We can ask Rosette to find the code that satisfies a specification.

(define-symbolic c integer?)
(define (mystery x) (+ x c))

; Find a value for 'c' such that mystery(5) = 10
(solve (assert (= (mystery 5) 10)))
; Result: (model [c 5])

It discovered that c must be 5! This is program synthesis.

Summary

Rosette powers real-world verification tools for file systems, weak memory models, and JIT compilers. It highlights Racket's ability to host languages that do things standard languages can't even dream of.