Rosette is a solver-aided language for program synthesis and verification | Heykuki News