Coq를 공부해보겠다는 막연한 목표와 함께 이런저런 자료를 찾아보고 그만두기를 반복하던 중, DeepSpec Summer School 세미나에서 나온 영상을 발견했다. 유투브에서 찾은 다른 영상들이 4,5년 전 자료였던 반면 DeepSpec에서는 최근인 2017, 2018년까지 꾸준히 학습자료와 세미나 영상이 업로드되고 있다.
사실 예전 LaTeX을 익힐 때에도 이것저것 찾아보기만 하다가 결국 학교 과제를 LaTeX으로 작성해보고서야 익숙해졌는데, 이번에도 실 사용 없이 공부하는게 얼마나 갈지는 잘 모르겠다.. 자료 초반에 “All the core chapters are suitable for both upper-level undergraduate and graduate students.” 라는 말이 있던데, 물론 저런 말들이 다 그렇듯이 전부 거짓말이겠지만 이젠 undergraduate 신분이라는 핑계도 사라졌으니 좀더 확실히 짚고 넘어가야겠다는 생각도 든다.
Overview
<Software Foundations> 라는 제목에서 짐작할 수 있듯이, 이런 것들을 하는 주된 목표는 “Building reliable software"라고 할 수 있다. 현대 사회에서 소프트웨어의 영향력이나 그만큼 커진 보안의 중요성에 대해서는 굳이 이 글이 아니어도 여러 곳에서 들었을 테니 생략하고, 다음 질문인 “그럼 어떻게 하면 reliable한 소프트웨어를 만들 수 있는가” 로 넘어가자. 다양한 시각에서 다양한 해결책이 제시되었다.
- 소프트웨어를 제작하는 사람을 중심으로 생각
- 익스트림 프로그래밍, 애자일, 폭포수 모델, ⋯
- SW 라이브러리를 디자인하는 방식 제안
- MVC모델, publish-subcribe, ⋯
- 프로그래밍 언어 자체의 설계철학을 제시
- OOP, aspect-oriented, functional, ⋯
- 소프트웨어의 성질을 수학적으로 논증(reasoning)
- SMT solver, Isabelle, Coq, ⋯
여기서 다루고자 하는 건 마지막 접근방식이다. 특히, <Software Foundations>에서는 크게 다음 3가지를 중점적으로 다룬다.
- 프로그램의 성질을 정밀(precise)하게 묘사하기 위한 Logic
- 엄밀한 논증을 위해 proof assistant를 사용하는 방법
- 프로그래밍과 논리를 잇는 연결고리로서의 functional programming
Proof Assistant
논리학이 CS에 제공하는 게 많아보이지만 의외로 CS가 논리학에 준 도움 또한 존재한다. CTF를 해봤거나 퍼즐 문제를 좋아한다면 한번쯤 들어봤을 SMT solver를 비롯해 다양한 툴이 있으며, 이는 크게 두 부류로 나뉘어진다
Automated Theorem Prover
명제를 입력하고 작동시키면 True 혹은 False를 리턴해주고, 필요한 경우 어떻게 그 결과가 나왔는지 근거를 제공한다. 예를 들어 \( A \land (B \lor \neg C)\)라는 명제에 True와 함께 A:True, B:True, C:False를 출력하는 식이다. 다룰 수 있는 범위에 다소 제약이 있으며, 모든 경우를 해결해주지는 못한다(ex: ran out of time 에러). SAT solver나 SMT solver, model checker 등이 있다.
Proof Assistant
proof assistant는 사람의 개입을 가능하게 해 직관을 더하면서도 증명에서 논증의 단단함은 잃지 않도록 한 일종의 하이브리드 도구라고 할 수 있다. 툴과 사람이 상호작용을 통해 증명을 완성해가며, Isabelle이나 ACL2, Coq 등이 있다.
Coq 활용 사례
Coq는 현재 전산학과 수학의 여러 분야에 폭넓게 활용되고 있다.
- 프로그래밍 언어의 모델링 플랫폼
- JavaCard 플랫폼의 보안성을 증명해 CC인증을 받는 데 활용됨
- 증명된(formally certified) SW나 HW의 개발환경
- CompCert(fully-verified C optimizing compiler), CertiKos(fully-verified hypervisor), CertiCrypt 등
dependent type을 이용한 함수형 프로그래밍 환경 제공
- higher-order logic에서의 proof assistant
- 4색 정리, Feit-Thompson 정리의 증명 및 검증