언어와 컴파일러 함께 정의
실행할 언어의 문법과 타입 규칙, 동작 의미를 정의하고 컴파일 과정을 검증한다. 저장소의 컴파일러 구성에는 구문 분석과 타입 추론, 어셈블리 변환과 코드 생성 단계가 포함된다. 소스가 어떤 의미를 갖는지가 검증의 출발점이다.
검증된 프로그램 제작 기반
HOL 함수에서 CakeML 프로그램으로 옮기며 증명을 생성하는 번역기를 제공한다. 관련 기반을 이용한 검증 예제와 라이브러리도 있다. 컴파일러의 정확성과 특정 프로그램이 원하는 기능을 수행한다는 성질은 각각 확인해야 한다.
구성 요소의 경계
프로젝트에는 검증된 부분뿐 아니라 검증되지 않은 보조 도구도 포함된다. 전체 저장소의 모든 파일이 같은 보장을 갖는다고 이해하면 안 된다. 재현 작업에서는 HOL4 환경과 컴파일러 버전, 사용하는 도구의 증명 범위를 함께 확인한다.
관련 문서
HOL4 / CompCert / Sail 명세 언어 / Lem 의미론 도구