Library Preface_ko_utf8

머리말


환영합니다

_소프트웨어 기초_(신뢰성 있는 소프트웨어의 수학적 기초)의 다양한 면들에 대한 전자책 시리즈의 시작점입니다. 강의 주제로 논리의 기본 개념, 컴퓨터를 활용한 명제 증명(Computer-assisted theorem proving), 콕 증명 보조기 (Coq proof assistant), 함수형 언어 (functional programming), 실행 과정 기반 의미 구조(operational semantics), 호어 논리(Hoare logic), 타입 시스템(static type system)을 다룬다. 고학년 학부생부터 박사과정 학생과 연구자들까지 다양한 독자들을 대상으로 한다. 논리나 프로그래밍 언어에 대한 사전 지식이 필요하지 않지만 수학을 많이 접했다면 도움이 될 것이다.
이 강의의 특징은 백 퍼센트 형식화해서 컴퓨터로 검사하도록 구성된 것이다. 즉, 전체 텍스트가 콕 스크립트다. 콕의 대화식 세션을 따라 텍스트 내용을 읽도록 구성되어 있다. 텍스트의 모든 상세 내용은 콕으로 완벽하게 형식화되어 있고, 대부분의 연습문제들을 콕을 사용하여 풀어보도록 설계되었다.
강의 파일들은 대략 한 학기 분량의 핵심적인 장들을 나열하도록 구성되어 있고, 일관성 있고 단일 방향성의 이야기로 구성되어 있다. 더불어 추가적인 주제들을 다루는 많은 파생된 장들도 있다. 모든 핵심적인 장들은 고학년 학부생과 대학원생들에게 적합하다.
이 책, _논리적 기초_,는 다른 책들을 위한 토대이고, 독자들에게 함수형 프로그래밍, 건설적 논리(constructive logic), 콕 증명 보조기를 소개한다.

개요

신뢰성 있는 소프트웨어를 만드는 것은 어렵다. 현대 시스템들의 크기와 복잡도, 개발에 참여하는 많은 개발자들, 다양한 시스템 요구사항들로 인해 100% 보다 훨씬 낮은 정확성이라도 대략 정확하게 소프트웨어를 만드는 것조차도 매우 어렵다. 그리고 사회의 다양한 국면과 엮여 정보를 처리함에 따라 버그와 위험으로 인한 비용이 확대된다.
컴퓨터과학자들과 소프트웨어 공학자들은 이러한 문제들에 대응하기 위해 소프트웨어 신뢰성을 높이기 위한 다양한 기법들을 개발했다. 소프트웨어 프로젝트 팀들을 관리하는 방법(예를 들어 익스트림 프로그래밍)에서부터 라이브러리(예를 들어 모델 뷰 컨트롤러, 발행-가입, 등)와 프로그래밍 언어(예를 들어 객체지향 프로그래밍, 관점 지향 프로그래밍,...) 설계 철학들, 소프트웨어의 성질들을 기술하고 추론하는 수학적 기법과 이 성질들을 검증하기 위한 도구들까지 다양하다. 이 강의는 마지막에 언급한 기법들에 초점을 맞춘다.
이 책은 세 가지 개념들을 엮어놓았다.
(1) 프로그램에 대한 명제를 정밀하게 만들고 정당화하는 _논리_의 기본 도구들
(2) 논리적 주장을 엄밀하게 만들기 위하여 _증명 보조기_를 사용
(3) 프로그램들에 대한 추론을 단순화하는 프로그래밍 방법으로 그리고 프로그래밍과 논리를 연결하는 역할로써 _함수형 프로그래밍_ 후기 장에서 추가적으로 읽을만한 문헌을 소개한다. 모든 참고문헌들에 대한 서지 정보는 Bib 파일에 있다.

논리

논리는 _증명_을 주제로 하는 학문 분야다. 증명이란 특정 명제들이 참인지 거짓인지에 대한 부정할 수 없는 주장이다. 컴퓨터과학에서 논리의 중요한 역할에 대해 설명하는 많은 책들이 있다. 마나(Manna)와 월딩거(Waldinger)는 논리를 "컴퓨터과학의 계산법"이라 불렀고, 할러펜(Halpern)과 그 동료들의 논문 _컴퓨터과학에서 논리의 유별난 효과_에서 논리가 어떻게 중요한 도구들과 통찰력들을 제공하는지 수십 가지 사례들을 나열하였다. 정말로 "사실 논리는 수학에서 보다 컴퓨터과학에서 훨씬 더 효과적임이 밝혀졌다. 특히 지난 백 년간 논리 발전의 많은 자극이 수학으로부터 왔기 때문에 이 사실은 상당히 주목할만하다."라고 보았다.
특히 _귀납적 증명_이라는 기초적인 도구들은 컴퓨터과학의 모든 영역에 사용된다. 독자 여러분은 분명히 이전에, 아마도 이산수학이나 알고리즘 분석에 관한 강의에서 이것들을 보았을 것이다. 하지만 이 강의에서 훨씬 더 깊이 이것들을 살펴볼 것이다.

증명 보조기

논리와 컴퓨터과학의 아이디어들은 서로 양쪽으로 주고받아왔다. 컴퓨터과학 또한 논리에 중요한 기여들을 해왔다. 그중 하나는 논리 명제들을 증명하는 것을 도와주는 소프트웨어 도구들을 개발해온 것이다. 이 도구들은 크게 두 가지로 분류할 수 있다.
  • _자동 정리 증명기_는 버튼만 누르면 제시한 명제가 _참_인지 _거짓_인지 (또는 _시간이 너무 오래 걸려 모른다_)를 리턴한다. 비록 특정 영역들에 국한되어 있지만 근래에 이 기술이 크게 발전해왔고 이제 다양한 상황들에서 사용되고 있다. 이 도구들의 예를 들면 에스에이티(SAT, boolean SATisfiability) 도구들, 에스엠티(SMT, satisfiability modulo theores) 도구들, 모델 검사기들이 있다.
  • _증명 보조기_는 어려운 부분들은 사람의 가이드에 의존하되 다소 반복적인 부분들을 자동화하여 증명하는 혼합형 도구이다. 널리 사용 중인 증명 보조기들로 이사벨(Isabelle), 아그다(Agda), 트웰프(Twelf), 에이씨넬투(ACL2), 피브이에스(PVS), 콕(Coq) 등이 있다.
이 강의에서는 콕을 사용한다. 증명 보조기 콕은 1983년에 개발을 시작했고 최근에 연구와 산업에 종사하는 다양한 커뮤니티에서 사용하고 있다. 콕은 대화식으로 형식적 추론을 만들고 컴퓨터가 확인하는 방식을 위한 다양한 기능을 제공하는 환경이다. 콕 시스템의 핵심부는 간단한 증명 검사기로 구성되어 있는데, 이 검사기를 통해 오직 정확한 추론 단계들만 수행하도록 보장한다. 콕 환경은 이 핵심부에 증명 개발을 도와주는 고급 기능들을 제공한다. 방대한 공용 정의들과 보조 정리들 라이브러리, 복잡한 증명들을 반자동으로 만들 수 있는 강력한 전술(함수), 특정 상황에 맞추어 증명 자동화 전술을 새롭게 정의할 수 있는 특별한 목적의 프로그래밍 언어 등이 포함되어 있다.
콕은 컴퓨터과학과 수학을 넘나드는 거대하고 다양한 분야의 중요한 성공 요소가 되고 있다.
  • _프로그래밍 언어를 모델링하는 플랫폼_으로써 복잡한 언어 정의들을 기술하고 추론하는 표준 도구가 되었다. 자바카드(JavaCard) 플랫폼의 보안성을 검사하는 데 사용되어 보안 분야 인증 표준 CC(Common Criteria)의 최고 등급을 받았다. x86과 LLVM 어셈블리 언어와 C와 같은 프로그래밍 언어의 형식 명세를 기술하는 데 사용되었다.
  • _형식적으로 검증된 소프트웨어와 하드웨어를 개발하기 위한 환경_으로써 사용되고 있다. 콤써트(CompCert) 프로젝트에서 C언어 최적화 컴파일러를 완벽하게 검증하였고, 써티코스(CertiKos) 프로젝트에서 하이퍼바이저를 완전히 검증하였으며, 부동소수점 숫자에 관한 알고리즘들의 정확성을 증명했고, 써티크립트(CertiCrypt) 프로젝트에서 암호 알고리즘들의 보안성을 추론하는 환경의 기초로 이용하고 있다. 오픈소스 리스크 파이브(RISC-V) 프로세서의 구현을 검증하는 데에도 사용 중이다.
  • _종속 타입(dependent types)을 제공하는 함수형 프로그래밍을 위한 제대로 된 환경_으로써 수많은 혁신들에 영향을 끼쳤다. 예를 들어 와이놋(Ynot) 시스템은 "관계형 호어 추론" (_호어 논리_의 확장으로 이 강의에서 다룰 것이다) 방법을 콕에 녹여냈다.
  • _고차원 논리(higher-order logic)를 위한 증명 보조기_로써 수학 분야에서 많은 중요한 결과를 검증하는 데 사용되어 왔다. 증명 안에 복잡한 계산을 포함하는 기능을 제공함으로써 네 가지 색 정리(4-color theorem)의 증명을 처음으로 형식적으로 검증해냈다. 이렇게 검증하기 전에 이 증명은 프로그램을 사용하여 많은 상황들을 검사하는 부분이 포함되어 있기 때문에 수학자들 사이에서 증명으로 인정할 지에 관하여 논쟁이 있었다. 콕으로 형식화하여 프로그램을 실행하여 확인했던 부분의 정확성까지 포함해서 모든 부분을 검사하였다. 더 최근에는 페이트 톰슨 정리(Feit-Thompson theorem, 유한단순군의 분류에 관한 주요한 첫번째 단계)을 콕으로 형식화하는데 더욱 방대한 양의 노력을 기울이고 있다.
만일 콕이라는 이름에 대해 궁금하다면 인리아(INRIA, 콕을 개발한 프랑스 국립 연구소)에 있는 공식 웹 사이트에 언급된 설명을 보자. "일부 프랑스 컴퓨터과학자들은 그들이 만든 소프트웨어에 동물 종의 이름을 붙이는 전통을 가지고 있다. 카멜(Caml), 엘란(Elan), 폭(Foc), 폭스(Phox)는 이런 암묵적인 전통의 예들이다. 프랑스어로 '콕'은 수탉을 뜻하기도 하고, 콕이 기초로 하는 이론, 구성 계산법(Calculus of Constructions, CoC)의 머리글자들처럼 발음한다." 수탉은 프랑스의 국가 상징이기도 하며, 씨-오-큐(C-o-q)는 초기에 콕을 개발한 사람들 중 티에리 코쿠아(Thierry Coquand) 이름에 포함된 첫 번째 세 문자들이기도 하다.

함수형 프로그래밍

_함수형 프로그래밍_이라는 용어는 거의 모든 프로그래밍 언어에서 사용할 수 있는 프로그래밍 스타일들을 가리키기도 하고 이 스타일들을 강조하여 설계된 프로그래밍 언어들을 말하기도 한다. 하스켈(Haskell), 오캐멀(OCaml), 에스엠엘(Standrad ML), 에프샵(F#), 스칼라(Scala), 스킴(Scheme), 라킷(Racket), 리스프(Common Lisp), 클로져(Clojure), 얼랑(Erlang), 콕 등이 함수형 프로그래밍 언어이다.
함수형 프로그래밍은 수 십 년간 발전되어 왔다. 그 기원은 처치(Church)가 1930년대에 발명한 람다 계산법(lambda calculus)이다. 이 시기는 초기 컴퓨터들(적어도 초기 전자 컴퓨터들) 보다 앞선다! 하지만 90년대 초에 이르러서야 비로소 산업계 엔지니어들과 언어 설계자들이 많은 관심을 보이기 시작했고 제인 스트리트 캐피털(Jane St. Capital), 마이크로소프트(Microsoft), 페이스북(Facebook), 에릭슨(Ericsson)과 같은 회사들의 고부가가치 시스템들에서 중요한 역할을 담당하고 있다.
함수형 프로그래밍의 가장 기본적인 생각은 가능한 계산은 _순수(pure)_해야 한다는 것이다. 즉, 실행 결과는 오로지 결과를 내는 것이라는 것이다. 입출력(I/O), 변수의 값을 할당, 포인터를 변경하는 것과 같은 _부작용(side effects)_은 없어야 한다는 생각이다. 예를 들어, _명령 기반(imperative)_ 정렬 함수는 숫자들 리스트를 받아서 숫자들을 가리키는 포인터들을 배열해서 그 리스트 안에 순서대로 놓도록 작성한다면, 순수한 정렬 함수는 원래 리스트를 받아서 그 리스트의 숫자들을 정렬된 순서로 담고 있는 _새로운_ 리스트를 리턴한다.
이런 스타일로 프로그래밍하면 프로그램을 이해하기 쉽고 추론하기 쉬운 형태로 작성할 수 있는 혜택이 있다. 자료구조에 대해 연산할 때 마다 항상 원래 자료구조는 변경하지 않은 채 두고 모두 새로운 자료 구조를 결과로 낸다면 이 자료구조를 공유하는 방식을 고민할 필요가 없고, 프로그램의 한 부분을 실행해서 변경이 발생함으로 인해 프로그램의 다른 부분이 의존하는 불변 성질을 깨뜨리지 않을까 걱정할 필요도 없다. 이러한 사항들은 동시성을 사용하는 시스템들에서 특히 중요하다. 동시성 시스템(concurrent systems)에서 변경 가능한 상태를 여러 스레드들이 공유하는 것은 치명적인 버그들의 잠재적 원인이다. 산업계에서 최근에 함수형 프로그래밍에 관심을 보인 많은 부분들이 동시성이 존재하는 상황에서 더 간단하게 동작하도록 프로그래밍할 수 있기 때문이다.
최근에 함수형 프로그래밍에 환호하는 또 다른 이유는 첫 번째 이유와 연관되어 있는데, 보통 함수형 프로그램들은 명령 기반 프로그램들 보다 병렬화가 훨씬 더 쉽기 때문이다. 만일 프로그램을 실행했을 때 결과를 내는 것 말고 특별히 다른 효과가 없다면 이 프로그램을 어디에서 실행하든 상관없다. 비슷한 얘기로, 프로그램을 실행하면서 자료구조가 내부적으로 결코 변경되지 않는다면 프로세서 코어들 또는 네트워크를 넘어서 이 자료구조를 자유롭게 복사할 수 있다. 하둡(Hadoop)과 같은 대용량 분산 질의 처리기들의 핵심이고 구글(Google)에서 전체 웹을 색인하는 데 사용하는 "맵-리듀스(Map-Reduce)" 프로그래밍 스타일은 함수형 프로그래밍의 고전적인 예이다.
이 강의의 목적을 위하여 함수형 프로그래밍은 앞서 언급한 장점과 더불어 또 다른 중요한 매력이 있다. 논리와 컴퓨터과학을 연결하는 다리 역할을 하는 것이다. 정말로 콕은 그 자체로 작지만 매우 표현력이 높은 함수형 프로그래밍 언어와 논리적 주장들을 서술하고 증명하는 데 사용할 도구들의 집합을 조합해놓은 것이다. 더욱이 더 자세히 들여다보면 콕의 논리에 관한 것과 프로그래밍에 관한 것은 콕 시스템의 동일한 기초 원리(underlying machinery)를 보는 다른 관점 들일뿐이라는 것을 발견한다. 즉, _증명과 프로그램_.

더 자세한 내용

이 책은 자체로 모든 내용을 담으려 했지만 특정 주제들을 더 깊이 탐구하고자 하는 독자들은 후기 장에서 더 자세한 내용에 대한 제안을 참고할 수 있다.

강의 진행을 위한 참고


책의 장들 간 의존성

이 책의 모든 장들 간의 의존성을 보여주는 다이어그램과 내용들을 연결하는 경로들을 deps.html 파일에서 확인할 수 있다.

시스템 요구사항

윈도우, 리눅스, 맥 운영체제에서 콕을 실행할 수 있다. 필요한 사항은:
  • 콕 웹 사이트에서 제공하는 콕을 설치. 8.6 버전을 사용하면 된다.
  • 콕을 대화식으로 사용하기 위해 필요한 통합개발환경(IDE). 현재 두 가지 선택이 가능하다.
    • 프룹 제너럴(Proof General)은 이맥스 기반 통합개발환경이다. 이맥스에 익숙한 사용자가 선호하는 선택이다. 콕과 별도의 설치가 필요하다 (구글링 "Proof General").
      이맥스를 사용하는 콕 사용자들 중 대범한 사용자라면 확장 기능들 company-coqcontrol-lock을 내려받아 사용할 수도 있다.
    • CoqIDE는 간단한 독립적인 통합개발환경이다. 콕과 함께 배포되기 때문에 콕을 설치하면 바로 사용 가능하다. 처음부터 컴파일해서 사용할 수도 있는데 어떤 환경에서는 그래픽 사용자 인터페이스 라이브러리 등 추가 패키지들을 설치해야 컴파일 가능하다.

연습문제

각 장은 많은 연습문제들을 포함하고 있다. 각 연습문제에 별 등급을 매겨 놓았다.
  • 별 하나: 쉬운 연습문제로 등급을 표시해두었다. 대부분의 독자들은 1,2분 내에 풀 수 있을 것이다. 이 별 등급의 연습문제들을 만날 때마다 풀어보는 습관을 갖기 바란다.
  • 별 두 개: 간단한 연습문제들 (5~10분).
  • 별 세 개: 다소 생각을 요구하는 연습문제들 (10분에서 30분).
  • 별 네 개와 다섯 개: 더 어려운 연습문제들 (30분 이상).
어떤 연습문제들에는 "고급(Advanced)"을 붙여 놓았고 다른 연습문제들은 "선택(optional)"을 붙여 놓았다. 선택 사항이 아니고 고급 연습문제들이 아닌 연습문제들만 푸는 것만으로도 핵심적인 내용을 잘 커버할 것이다. 선택적 연습문제들은 핵심 개념들과 함께 다소 추가적인 연습을 제공하고 일부 독자들에게 흥미를 줄 수 있은 부차적인 주제들을 소개한다. 고급 연습문제들은 도전적이고 깊은 내용을 원하는 독자들을 위한 것이다.
_이 연습문제들에 대한 풀이들을 공공장소에 공개하지 않을 것을 부탁한다._ 소프트웨어 기초는 스스로 학습과 대학 강의에 널리 사용되고 있다. 해답이 쉽게 노출된다면 과제물을 가지고 성적을 주는 일반 강의에 훨씬 덜 도움이 될 것이다. 특히 독자들에게 검색 엔진으로 찾을 수 있는 어떠한 장소에도 연습문제들의 해답을 올리지 않도록 요청한다.

콕 파일들을 내려받기

이 책의 배포판에 대한 전체 소스를 포함하는 묶음(tar) 파일에 콕 스크립트와 에이치티엠엘(HTML) 파일들이 있는데 아래 주소에서 제공한다.
http://www.cis.upenn.edu/~bcpierce/sf
(만일 이 책을 강의의 일부로 사용한다면 그 강의를 담당하는 교수가 이 파일들을 직접 수정한 버전을 제공할 수도 있다. 배포판 대신 수정판을 사용하세요)

강의 비디오

_논리적 기초_에 관한 집중 여름 강좌들_(2017년 딥스펙 여름 학교의 일부)을 아래 주소에서 볼 수 있다. 처음 강의 동영상의 화질이 좋지 않지만 나중에는 점점 나아질 것이다.

    - https://deepspec.org/event/dsss17/coq_intensive.html


강사를 위한 메모

강사 본인의 강의에 이 책을 사용한다면, 내용 중에 변경하고, 개선하고, 추가하고 싶은 것이 반드시 있을 것이다. 당신이 기여하는 것을 환영합니다!
만일 라이센스 문구, 서브라이센스 등을 조정해야하는 상황이 발생하는 경우 합법성 문제를 단순하게 유지하고 책임을 단일화하기 위해서 이 책에 기여하는 모든 사람들(개발자 저장소를 접근하는 모든 사람들)에게 각자의 기여한 바에 대한 저작권을 다음과 같이 적절한 "기록의 저자(Author of Record)"에 부여할 것을 요청한다.
  • 나는 나의 과거와 미래에 기여했던 바에 대한 저작권을 소프트웨어 기초 프로젝트에 각 권 또는 요소의 "기록의 저자"에 부여하고, 소프트웨어 기초의 나머지와 동일한 조항하에 라이센스를 부여한다. 현재 시점에 "기록의 저자"는 다음과 같음을 이해하고 있다. 2016년까지 "소프트웨어 기초"로, 2016년부터 각각 "논리적 기초"와 "프로그래밍 기초"로 알려진 1권과 2권에 대해 "기록의 저자"는 벤자민 피어스이다. 3권 "함수형 알고리즘 검증"에 대해 "기록의 저자"는 안드류 더블류 아펠이다. 이 범위 밖에 있는 요소(예를 들어 타입 세팅, 채점 도구, 다른 기반 소프트웨어)들에 대해 "Author of Record"는 벤자민 피어스이다.
시작하려면 벤자민 피어스에게 본인 소개와 이 책을 사용할 계획을 서술한 이메일을 보내주세요. 그리고 아래 내용도 함께 보내주세요. (1) 위의 저작권 위임 텍스트와 (2) 명령어 "htpasswd -s -n NAME"를 실행한 결과 원하는 사용자 이름을 정해서 NAME을 바꾸면 됩니다.
서브버전 저장소와 개발자 메일 리스트에 접근할 수 있도록 설정할 것입니다. 이 저장소의 INSTRUCTORS 파일에서 추가 지시 사항들을 확인할 수 있습니다.


번역

번역을 자원해서 진행하는 팀의 노력 덕분에 http://proofcafe.org/sf에서 일본어로 _소프트웨어 기초_를 읽을 수 있습니다. 중국어 번역은 진행 중입니다.


감사

_소프트웨어 기초_ 시리즈를 개발하는 것을 국립과학재단 엔에스에프 익스페디션 그란트 1521523, _딥 스펙에 관한 과학_으로부터 일부 지원을 받았습니다.