답변내용
Coq 증명 보조기는 두 영역으로 나누어져 있습니다.
하나는 논리증명 영역이고, 다른 하나는 완성된 증명의 안전성을 확인하는 검증영역입니다. 논리증명 영역은 수리논리학자들이 기존에 세워 놓은 이론을 코드로 구현한 영역이고, 검증영역은 논리증명 영역에서 생성된 모든 증명과 프로그램이 지정된 결과를 제대로 도출하는가 여부를 최종 확인하는 영역입니다.
논리증명 영역은 기존의 수리논리 이론에 대한 연구결과를 통해 검증되었다고 봅니다. 반면에 검증영역의 경우는 좀 더 어렵습니다. 검증영역은 Coq의 핵심이며 따라서 커널(kernel)에 포함되어 있습니다. 그런데 커널을 구현하는 코드는 3천여 줄에 불과합니다. 따라서 사람들이 섬세한 부분까지 직접 눈으로 조심스럽게 검증을 합니다. 물론 다양한 검증 도구를 이용하기도 합니다. 이런 식으로 사람이 직접, 아니면 도구들 간의 상호검증 방식을 이용합니다.
물론 언급된 방식은 100% 안전성을 보장하지 못합니다. 사실, 어떤 방식을 이용한다 하더라도 Coq과 같은 도구를 100% 검증하는 일은 불가능합니다. 그래서 개발자들은 커널 부분을 절대로 크게 만들지 않습니다. 예상못하는 문제를 피하기 위해서입니다. Automath라는 최초의 자동증명기를 구현한 드 브로인(de Bruijn)이라는 저명한 네덜란드 논리학자가 이미 1970년대에 이 문제를 언급하고 작은 커널을 사용해야 한다는 원칙을 제안하였는데, 그래서 \"드 브로인 원칙\"이라고 불리기도 합니다. - 이계식 드림(한경대 컴퓨터공학과 교수)
