언어 안에서 분석 구성
검증 질문을 외부 해결기에 따로 적는 대신 프로그램을 작성하는 과정에서 기호값과 조건을 표현한다. Rosette는 도메인 전용 분석 언어를 만드는 기반으로도 활용할 수 있다. 합성할 대상과 만족해야 할 조건은 사용자가 정해야 한다.
안전한 구성의 의미
rosette/safe는 기호값과 함께 안전하게 사용할 수 있는 구성으로 범위를 제한한다. 전체 rosette 언어에서는 Racket 기능을 폭넓게 사용할 수 있지만, 기호값을 지원하지 않는 기능에 전달하지 않도록 프로그래머가 판단해야 한다.
실행과 기호 의미 구분
일반 값으로 잘 동작하는 Racket 코드라도 기호값에서 같은 의미를 유지한다고 볼 수 없다. 안전하지 않은 구성은 예외뿐 아니라 잘못된 의미를 만들 수 있다. 도구가 처리하는 언어 범위와 분석용 프로그램의 동작을 함께 검토한다.