명제와 증명을 함께 작성
수학적 정의나 프로그램의 명세를 형식 언어로 표현하고 증명을 구성한다. 타입 이론에 기반한 핵심 검사기가 증명 산출물을 확인한다. 표면적으로 그럴듯한 설명이 아니라 정해진 규칙에 맞는 형식적 구성이 필요하다.
증명 작업의 자동화
전술과 보조 도구는 증명의 세부 단계를 만드는 데 도움을 준다. 자동화된 탐색을 사용하더라도 확인한 명제와 사용한 가정의 의미를 검토해야 한다. 명세가 실제 요구 사항과 다르면 올바른 형식 증명만으로 그 간격이 없어지지는 않는다.
프로그램 개발과 연결
정의에서 OCaml이나 Haskell 같은 실행 코드로 추출하는 기능을 제공한다. CompCert와 여러 수학 형식화 프로젝트가 관련 생태계를 활용한다. 예전 Coq 자료를 사용할 때는 이름뿐 아니라 버전과 패키지 호환성도 함께 맞춘다.
관련 문서
Agda / Idris 2 / CompCert / Lean 증명 도구