Computer Science as Infrastructure: the Spine of the Lean Computer Science Library (CSLib)

수학의 세계를 거대하고 오래된 도시라고 상상해 보십시오. 수 세기 동안 사람들은 각자 논리의 집을 지어왔지만, 종종 서로 다른 설계도를 사용했기에 도구를 공유하거나 새로운 구역을 함께 건설하는 데 어려움을 겪었습니다. 그러다 Mathlib이 등장했습니다. 이는 전 세계의 수학자들이 동일한 언어와 규칙을 사용하여 증명을 구축하기로 합의한 웅장하고 중앙 집중화된 도서관입니다. 이것은 마치 수학을 위한 보편적인 번역기와 같아서, 복잡하고 고립된 아이디어들을 모두가 어떻게 다리가 건설되었는지 정확히 확인하고 그 다리가 무너지지 않을 것이라고 신뢰할 수 있는, 공유되고 검증된 도시 경관으로 탈바꿈시킵니다.

이제 컴퓨터 과학이 건설되기를 기다리고 있는 다음 세대의 위대한 도시라고 상상해 보십시오. 컴퓨터 과학은 우리가 기계에게 어떻게 생각하고, 움직이고, 문제를 해결하도록 명령할 것인가를 연구하는 학문입니다. 하지만 과거의 수학 도시와 마찬가지로, 컴퓨터 과학은 종종 고립된 작업실들의 집합체였습니다. 이 논문은 Mathlib이 수학에 했던 것처럼 컴퓨터 과학을 위해 무엇을 할 것인지 목표로 하는 새로운 프로젝트인 CSLib을 소개합니다. 여기서 핵심적인 질문은 단순하지만 매우 거대합니다. 우리가 소프트웨어와 모델을 공식적으로 검증할 수 있을 만큼 견고하고 표준화된, 컴퓨터 과학의 "척추"를 구축할 수 있을까요? 만약 우리가 그렇게 할 수 있다면, 이는 단순히 오류를 찾기 위해 테스트에만 의존하는 것이 아니라, 수학적으로 검증된 속성을 가진 디지털 시스템을 구축할 수 있음을 의미합니다.

디지털 도시의 새로운 중추

CSLib을 성장하는 디지털 도시의 중추 신경계라고 생각하십시오. 도시가 마천루와 다리를 지탱하기 위해 튼튼한 척추를 필요로 하듯, 컴퓨터 과학은 우리가 매일 사용하는 복잡한 소프트웨어를 지원할 수 있는 검증된 규칙의 견고한 토대가 필요합니다. 이 논문은 그 척추의 설계도를 제시합니다. 이 프로젝트는 단순히 몇 개의 임의적인 방을 만드는 것이 아닙니다. 이 도서관에 참여할 모든 사람이 동의하여 사용할 기초 원칙, 운영 규칙, 그리고 의미론적 프레임워크(프로그램에 대해 이야기하는 방식에 대한 "사전과 문법"이라는 멋진 표현입니다)를 놓는 작업입니다.

저자들은 거인들의 어깨 위에서 이 도서관을 구축하고 있으며, 특히 Mathlib의 발자취를 따르고 있습니다. 그들은 순수 수학에서 성공했던 동일한 레시피를 가져와 이를 복잡하고 실용적인 컴퓨터 과학의 세계에 적용하고 있습니다. 목표는 프로그래밍 언어와 소프트웨어 모델에 관한 아이디어들이 어디서나, 누구라도 저장하고, 확인하고, 재사용할 수 있는 장소를 만드는 것입니다.

도구들

이 도서관이 작동하게 만들기 위해, 이 논문은 우리 디지털 도시의 건설 장비 역할을 하는 영리한 도구들을 소개합니다.

첫째, 그들은 **재사용 가능한 의미론적 인터페이스(reusable semantic interfaces)**를 구축했습니다. 여러분이 비디오 게임 캐릭터의 움직임을 설명하려고 한다고 가정해 봅시다. 모든 애니메이션 프레임을 하나하나 설명할 수도 있지만, "플레이어가 'A' 버튼을 누르면 캐릭터가 점프한다"와 같은 표준화된 규칙 세트를 사용할 수도 있습니다. CSLib에서 저자들은 두 가지 특정 유형의 움직임에 대한 표준 "규칙서"를 만들었습니다: 리덕션(reduction)(프로그램이 단계별로 스스로를 단순화하는 방식)과 레이블된 전이 시스템(labelled transition systems)(프로그램이 빨간불에서 초록불로 바뀌는 신호등처럼 한 상태에서 다른 상태로 이동하는 방식)입니다. 이것들은 일회성 설명이 아니라 재사용 가능한 인터페이스입니다. 즉, 새로운 프로그래밍 언어에 대한 무언가를 증명하고 싶을 때, 바퀴를 다시 발명할 필요가 없습니다. 기존의 신뢰할 수 있는 규칙서에 여러분의 새로운 언어를 그대로 끼워 넣기만 하면 됩니다.

둘째, 이 논문은 **증명 자동화(proof automation)**를 강조합니다. 과거에 소프트웨어가 올바른지 증명하는 것은 벽의 벽돌 하나하나를 수동으로 확인하는 것과 같았습니다. 그것은 느리고 인간의 실수에 취약했습니다. 저자들은 증명을 확인하는 것을 돕는 슈퍼 fast 로봇 조수와 같은 도구들을 기여했습니다. 이 자동화는 인간이 코드의 모든 줄을 뚫어지게 쳐다보지 않고도 논리가 성립하는지 확인하도록 돕습니다. 이는 마치 지치지 않는 논리용 맞춤법 검사기를 갖는 것과 같습니다.

셋째, 그들은 CI/테스트 지원을 설정했습니다. 소프트웨어 세계에서 "CI"는 지속적 통합(Continuous Integration)을 의미하며, 이는 기본적으로 안전망입니다. 누군가 도서관에 새로운 조각을 추가할 때마다, 자동화된 시스템이 다른 부분을 망가뜨리지 않는지 확인합니다. 논문은 이 시스템이 새로운 컴퓨터 과학 라이브러리를 기존의 수학 라이브러리인 Mathlib과 호환되도록 설계되었다고 언급합니다. 이는 새로운 디지털 고속도로가 기존의 수학적 다리들과 완벽하게 연결되어, 두 세계 사이에서 교통이 원활하게 흐를 수 있도록 보장하는 것과 같습니다.

실제로 무엇이 있는가?

이 논문은 단지 도구에 대해서만 이야기하는 것이 아니라, 그것들이 이미 어떻게 사용되고 있는지를 보여줍니다. 저자들은 이 새로운 프레임워크 내에서 언어와 모델의 **첫 번째 실질적인 발전(first substantial developments)**을 기여했습니다. 이는 그들이 단순히 비계(scaffolding)를 세운 것이 아니라, 실제로 첫 번째 건물들을 짓기 시작했다는 것을 의미합니다. 그들은 프로그래밍 언어와 모델의 실제 개념들을 가져와 새로운 시스템을 사용하여 성공적으로 형식화했습니다.

하지만 달성된 성과의 범위를 이해하는 것이 중요합니다. 이 논문은 이것들을 기초 원칙이자 초기 개발 단계로 제시합니다. 이는 이 접근 방식이 작동하며 미래를 위한 견고한 프레임워크를 제공한다는 것을 시사하지만, 컴퓨터 과학의 모든 문제를 해결했다고 주장하는 것은 아닙니다. 이 작업은 "급속히 성장하는" 라이브러리로 묘사되며, 이는 여전히 건설 중인, 살아 숨 쉬는 프로젝트임을 암시합니다. 저자들은 토대가 견고하고 첫 번째 방들에 가구가 배치되었다는 것을 보여주고 있지만, 도시는 아직 완성되려면 멀었습니다.

이것이 왜 중요한가

그렇다면 왜 호기심 많은 십 대가 형식화된 컴퓨터 과학 라이브리에 관심을 가져야 할까요? 왜냐하면 이것은 판지로 집을 짓는 것과 강철로 집을 짓는 것의 차이이기 때문입니다. 오늘날 우리는 소프트웨어를 작성할 때, 그것이 부서지는지 보기 위해 흔히 테스트를 합니다. 만약 부서지지 않는다면, 우리는 그것이 안전하다고 가정합니다. 하지만 CSLib를 통해 우리의 목표는 소프트웨어의 규칙과 모델이 엄격하게 검증될 수 있는 공유된, 검증된 라이브러리를 만드는 것입니다. 이러한 아이디어들을 중앙 집중화하고 확인 과정을 자동화하는 도구를 제공함으로써, 저자들은 핵심적인 속성들이 수학적으로 검증될 수 있는 소프트웨어 개발의 길을 닦고 있습니다.

논문은 이러한 아이디어들을 중앙 집중화하고 확인 과정을 자동화하는 도구를 제공함으로써, 우리 디지털 세계의 "척추"가 깨지지 않는 미래를 건설할 수 있다고 주장합니다. 이는 코딩의 혼돈이 수학의 질서에 의해 길들여져, 단순히 기능적인 것을 넘어 근본적으로 신뢰할 수 있는 디지털 풍경을 만드는, 유쾌하고 야심 찬 비전입니다.