궁금해 하시는 분들이 있는 것 같아 올려 봅니다.


Coq 용으로 가장 많이 추천하는 입문용 교재는 Software Foundations (https://softwarefoundations.cis.upenn.edu/). 이 책의 최대 장점은 텍스트 전체가 literate program code 라는 것. 개념을 자연어로 설명하는 주석과 컴퓨터가 읽을 수 있는 소스코드가 씨실과 날실처럼 교차하는 형태로 되어 있고, 주석을 읽으며 자기가 이해한 방식이 맞는지 바로 옆의 코드를 가지고 놀면서 실시간으로 확인할 수 있다는 뜻. 이건 독학을 할 때 특히 큰 장점인데, (사용자가 새로 만들어 낸 문제를 포함한) 모든 문제의 풀이를 즉시 채점해 주고 절대 실수하지 않는 조교가 붙어 있는 것과 마찬가지이기 때문.


다만 CS나 HW가 아닌 수학을 위해서 Coq가 최선의 선택인가? 는 좀 의문의 여지가 있다고 봅니다. 이건 본인이 증명기를 사용하는 목적이 무엇인지를 고려해 볼 필요가 있을 듯.