증명 작업을 프로그래밍하기
정리를 형식적으로 표현하고 작은 추론을 조합해 증명한다. 내장된 결정 절차와 자동 증명 기능은 단순한 목표를 처리하는 데 도움을 준다. 복잡한 명제에서는 사용자가 정의와 보조 정리, 증명 전략을 설계해야 한다.
외부 분석 도구와 연결
SMT나 BDD 엔진 같은 외부 프로그램에 접근하는 오라클 기구를 제공한다. 증명 작업에 어떤 외부 결과를 사용했는지에 따라 신뢰해야 하는 구성 요소를 구분해야 한다. 자동으로 결과가 나왔다는 사실만으로 모든 경로의 신뢰 조건이 같아지는 것은 아니다.
실행과 증명의 결합
HOL4는 추론과 실행, 속성 검사를 결합하는 기반으로 활용된다. CakeML처럼 언어와 컴파일러를 검증하는 프로젝트도 이 환경에서 개발된다. 형식 정의와 실제 대상의 연결, 사용한 가정을 함께 검토해야 증명이 보장하는 범위를 이해할 수 있다.