Rosette 介绍
Rosette 是新的计算机辅助解析编程（SDSLs）语言，扩展了 Racket
的一些特性：合成，验证，调试和执行。
Rosette 是一个解算器辅助的编程语言，扩展了 Racket
用于程序合成、校验等。为了校验和合成代码，Rosette 将其编译为带 SMT 解决逻辑的逻辑限制解算。
示例代码：
#lang Rosette (define (interpret formula) (match formula [`(∧ ,expr ...) (apply && (map interpret expr))] [`(∨ ,expr ...) (apply || (map interpret expr))] [`(¬ ,expr) (! (interpret expr))] [lit (constant lit boolean?)])) ; This implements a SAT solver. (define (SAT formula) (solve (assert (interpret formula)))) (SAT `(∧ r o (∨ s e (¬ t)) t (¬ e)))