[{"_1":2,"_35":-5,"_36":-5},"loaderData",{"_3":4},"routes/tape",{"_5":6,"_24":9,"_25":26},"initialTree",[7,15,18,21],{"_8":9,"_10":9,"_11":12,"_13":14},"name","+.00-Preface.tape","path","type","file","title","서문",{"_8":16,"_10":16,"_11":12,"_13":17},"+.01-Advance-for-the-Readers.tape","독자를 위한 조언",{"_8":19,"_10":19,"_11":12,"_13":20},"00.01-Starting-Out.tape","0. 시작하기",{"_8":22,"_10":22,"_11":12,"_13":23},"1-type-theory.tape","1. 타입 이론","initialFilePath","initialFile",{"_13":14,"_27":28},"cells",[29],{"_30":31,"_11":32,"_33":34},"id","46f10250-2cff-4b44-a83f-49720b6e0edf","prose","content","

〈An Infinitely Lengthy Tape〉는 Evan Chen 이 집필한 〈An Infinitely Large Napkin〉(이하 Napkin)에서 영감을 얻어 작성하게 되었다. 이름은 Napkin 원제에 튜링 기계 비유를 섞어 무한히 긴 테이프에 프로그램을 적어 내리듯, 소프트웨어 엔지니어링을 위한 아낌없이 담아보고자 한다.

책애 관하여

〈An Infinitely Lengthy Tape〉는 기본적으로 소프트웨어 공학과 관련 있는 주제라면 모두 포용하나, 첫 집필 주제는 Benjamin C. Pierce의 〈Software Foundations〉이나 Phillip Waddler와 Wen Kokke의 〈Programming Language Foundation in Agda〉, 〈The HoTT Book〉과 같은 형식적 검증(Formal Verification), 그리고 타입 이론(Type Theory)을 목표로 잡았다.

이 책은 Napkin처럼 스스로-온전한(Self-contained) 책이기를 희망했고, 그렇게 가장 바닥에서부터 구성적으로(Constructive) 쌓아 올라나가기를 택했다. 디지털 논리 회로의 추상화가 없다고 한다면 〈Nand to Tetris〉 같은 서적이 다루는 내용을 고려해볼 수 있겠으나 너무 먼 아랫단계 추상화 계층이고, 실무적으로 도움이 될 여지가 적다고 여겨 생략하였다. 그리하여, 〈An Infinitely Lengthy Tape〉는 그 다음으로 우리가 다뤄야 하는 언어에 대해 설명하고자 한다.

이 책의 목적은 어떠한 교과서를 대체하는 것이 아니다. 다만, 여러 고급 개념을 \"수박 겉 핥기\" 수준으로 배우며 다양한 문제를 접하고, 해결을 위한 방책을 깨닫는 과정을 전달하는 걸 목표로 한다. 그렇기에 이 책은 \"적당한\" 정의를 바탕으로 이해할 수 있게 구성한다. 다만, 적확한 정의와 동작을 찾고자 하는 이들을 위해 상세한 참조 문서를 남기도록 한다.

연습 문제는 쉽게 풀 수 있는 문제부터 교훈적인 \"어려운\" 문제까지 포함한다. 난이도 기호를 참고하라.

Napkin 철학

Napkin이 가진 철학은 가볍게 인용하겠다.

고급 수학을 가르치는 방법은 두 가지가 있다.
어떤 정리를 알려주되 왜 성립하는지는 안 알려주며 외우라고 강요하기
모든 세부사항을 증명하는 강의를 들으며 수마에 빠져들기
보통 첫번째 방법은 싫을 거다. 그래서 두번째 방법이 기본이지만, 가끔 빠져나갈 필요도 있다.
대학교 교과서와 달리, 이 책의 목표는 여러분을 가르치는 게 아니라, 재밌는 수학을 보여주는 것이다. 그래서 다른 책이라면 지루하게 늘어놓을 증명도 우리는 때때로 생략할 수 있다. 재미 없으니까. 물론 그게 왜 참이어야만 하는지 증명의 모티브는 제공할 것이다.
이 책은 자연스러운 설명이 증명보다 낫다고 믿는다.

크게 동의한다. 〈An Infinitely Lengthy Tape〉 역시 위 철학을 바탕으로 작성되었다.

감사의 말

이 책을 작성할 정도로 지식을 쌓게 도와준 스터디원들에게 먼저 감사를 표한다. 다음으로, 좋은 학습 자료를 만들어 공개해 준 수많은 저자들에게 경의를 표한다. Software Foundations, Napkin, The HoTT Book과 같은 훌륭한 저서 없이는 이 책이 탄생할 수 없었다. 다시 한 번 큰 감사를 표한다.

","actionData","errors"]