프로그래밍 언어 이야기를 하다 보면 늘 이런 고민이 나와요. 빠르게 돌아가는 코드를 쓰면 메모리 버그가 걱정되고, 안전한 언어를 쓰면 성능이 아쉽다는 거죠. Rust가 이 둘을 꽤 잘 풀어내면서 큰 사랑을 받았는데요, 사실 훨씬 전부터 이 문제를 더 극단적인 방식으로 파고든 언어가 있어요. 바로 ATS예요.
오늘 소개할 Introduction to Programming in ATS는 ATS를 만든 보스턴대학교 Hongwei Xi 교수가 쓴 무료 온라인 입문서예요. 새로 나온 책은 아니지만, AI가 코드를 대량으로 쏟아내는 요즘 '이 코드가 맞다는 걸 어떻게 확신하지?'라는 질문이 커지면서 다시 읽어볼 이유가 생겼거든요.
ATS가 뭐길래
ATS는 Applied Type System의 줄임말이에요. 겉모습은 OCaml이나 Standard ML 같은 함수형 언어와 닮았는데, C 코드로 컴파일되고 가비지 컬렉터 없이도 돌아갈 수 있어요. 여기에 두 가지 무기를 얹었어요. 의존 타입과 선형 타입이에요.
의존 타입이 뭐냐면, 타입 안에 값에 대한 정보를 넣는 기능이에요. 보통 언어에서 타입은 '이건 정수야'까지만 말하잖아요. 의존 타입은 '이건 0 이상이고 배열 길이보다 작은 정수야'까지 말할 수 있어요. 이해하기 쉽게 단순화해서 예로 들면 이런 모양이에요.
fun{a:t@ype}
safe_get {n:int} {i:nat | i < n}
(xs: arrayref(a, n), i: int(i)): a = xs[i]
중괄호 안의 i < n이 핵심이에요. 인덱스가 범위를 벗어날 가능성이 있는 코드는 컴파일 자체가 안 돼요. 런타임에 검사하는 게 아니라 컴파일러가 미리 따져보는 거라서, 실행 시점 비용이 없어요.
함수가 반드시 끝난다는 것도 표시할 수 있어요.
fun fact {n:nat} .<n>. (x: int(n)): int =
if x > 0 then x * fact(x-1) else 1
.<n>.는 재귀할 때마다 n이 줄어든다는 약속이에요. 이 약속을 어기면 컴파일러가 거절해요. 무한 재귀를 타입 검사 단계에서 잡아내는 셈이죠.
증명을 코드처럼 쓴다
ATS의 진짜 개성은 여기서 나와요. 프로그램 안에 수학 증명을 같이 쓸 수 있거든요. 대표적인 예시가 피보나치 수열의 정의예요.
dataprop FIB (int, int) =
| FIB0 (0, 0)
| FIB1 (1, 1)
| {n:nat} {r0,r1:int}
FIB2 (n+2, r0+r1) of (FIB (n, r0), FIB (n+1, r1))
이건 실행되는 코드가 아니라 '피보나치의 n번째 값이 r이다'라는 명제의 정의예요. 이렇게 정의해두면, 빠른 반복문으로 구현한 함수가 이 정의를 만족한다는 증명을 결과와 함께 돌려주게 만들 수 있어요. 테스트가 몇 가지 입력을 확인하는 일이라면, 증명은 모든 입력에 대해 확인하는 일이에요. 게다가 이런 증명은 컴파일이 끝나면 지워져서 최종 C 코드에는 남지 않아요. 안전성은 챙기고 성능 비용은 안 내는 구조죠.
선형 타입은 '딱 한 번만 써야 하는 값'이에요. 은행 창구 번호표를 떠올려 보세요. 쓰면 사라지고, 복사할 수도 없고, 안 쓰고 버려도 안 돼요. ATS는 메모리 소유권을 이 번호표처럼 다뤄요. 포인터를 읽으려면 '이 주소에 이런 값이 있다'는 증명을 함께 들고 있어야 하고요.
fun{a:t@ype}
ptr_read {l:addr} (pf: !a @ l | p: ptr(l)): a = !p
| 왼쪽이 증명, 오른쪽이 실제 값이에요. 덕분에 해제한 메모리를 또 쓰거나 해제를 빼먹는 실수가 컴파일 단계에서 걸러져요.
다른 언어와 비교하면
가장 많이 비교되는 건 Rust예요. Rust의 소유권은 '아핀 타입'에 가까워서 값을 안 쓰고 버리는 건 허용돼요. ATS의 선형 타입은 반드시 소비해야 해서 더 엄격하죠. 대신 Rust는 컴파일러가 알아서 추론해주는 부분이 훨씬 많고, 도구와 생태계도 비교가 안 될 만큼 좋아요. Rust가 '많은 사람이 쓸 수 있는 안전함'을 택했다면, ATS는 '표현할 수 있는 안전함의 한계'를 밀어붙인 쪽이에요.
의존 타입 쪽에서는 Idris, Lean, Rocq(옛 이름 Coq)가 있어요. 이들은 수학 증명이나 검증에 더 무게를 두고, 시스템 프로그래밍 성능은 주된 목표가 아니에요. ATS처럼 저수준 메모리 제어까지 한 언어에서 다루려는 시도는 드문 편이에요.
한국 개발자에게는 어떤 의미일까
솔직히 말하면 ATS를 회사 프로젝트에 도입할 일은 거의 없을 거예요. 커뮤니티가 작고, 라이브러리도 적고, 컴파일 에러 메시지는 악명 높을 만큼 읽기 어렵거든요. 그래도 이 책은 읽을 가치가 있어요. '타입으로 버그를 못 만들게 설계한다'는 사고방식을 가장 날것으로 배울 수 있으니까요.
이 사고방식은 일상 코드에도 바로 쓸 수 있어요. TypeScript에서 유니언 타입으로 불가능한 상태를 없애는 것도, Rust에서 타입 상태 패턴으로 잘못된 호출 순서를 막는 것도 같은 뿌리예요.
읽는 순서는 이렇게 추천해요. 앞부분의 함수형 기초는 OCaml이나 Haskell을 아신다면 빠르게 넘기고, 의존 타입 장에서 속도를 늦추세요. 그다음 증명과 뷰(view) 부분을 읽으면 돼요. 컴파일러는 patscc이고, 소스 파일 확장자는 .dats예요. 예제를 고쳐서 일부러 컴파일 에러를 내보는 게 가장 빨리 배우는 방법이에요.
마무리
한 줄로 정리하면, ATS는 실무 언어라기보다 '컴파일러가 어디까지 보장해줄 수 있는가'를 보여주는 교과서예요. AI가 코드를 더 많이 쓰게 될수록, 사람의 리뷰 대신 타입과 증명으로 검증하는 방식이 늘어날까요? 여러분은 어디까지 컴파일러에게 맡기고 싶으신가요?
🔗 출처: Hacker News