정의를 여러 체계에서 공유
같은 의미론을 실행 모델과 증명기에서 각각 다시 작성하면 정의 사이에 차이가 생길 수 있다. Lem은 하나의 정의를 여러 대상으로 옮기는 기반을 제공한다. 도메인 전용 도구가 생성하는 중간 언어로 사용하는 목적도 있다.
함수형 구성과 논리 표현
순수 함수와 재귀 자료형, 패턴 대응 같은 함수형 프로그래밍 구성에 집합과 관계, 양화 등 논리 표현을 결합한다. 대상 체계에 맞게 이름이나 표기, 표현을 조절하는 기능도 있다. 출력마다 자연스러운 표현이 완전히 같지는 않다.
출력과 증명은 다른 작업
정리 증명기용 정의가 생성되어도 그 정의의 원하는 성질이 자동으로 증명된 것은 아니다. 각 백엔드에서 필요한 라이브러리도 별도로 준비해야 한다. 프로젝트는 지속 사용과 활발한 개발 상태를 구분해 안내하므로 실제 환경의 호환성을 확인한다.
관련 문서
Ott 언어 정의 도구 / Sail 명세 언어 / Why3 / K 프레임워크