수학적 정의를 관리하기
문법과 판단 규칙을 일관된 표기로 작성하고 문서용 조판과 형식 정의에 활용한다. 정의를 파싱하면서 판단 형식이나 메타변수 표기의 불일치 같은 단순 오류를 찾을 수 있다. 문서가 생성된다는 사실과 논리적 성질이 증명된다는 사실은 다르다.
반복 작업 자동화
자유 변수와 치환, 하위 문법 검사 등에 필요한 정의를 생성하는 기능이 있다. 다른 문서나 증명 파일 안에 언어의 항을 넣고 처리하는 필터로도 사용할 수 있다. 각 출력 대상에 맞는 주석과 설정이 필요하다.
바인딩 표현의 경계
변수 바인딩을 표현하는 방식은 의미론 작업에서 중요한 선택이다. 완전하게 지원하는 구체 표현과 실험적 백엔드의 범위가 다르다. 알파 동치 같은 개념을 어떤 표현으로 다루는지 확인하고 자동 생성 결과를 검토해야 한다.
관련 문서
Lem 의미론 도구 / Sail 명세 언어 / K 프레임워크 / Dafny