요약
명세와 구현을 한 언어에 담는 ATS를 예제 중심으로 익히는 온라인 입문서입니다.
ATS는 프로그램과 그 프로그램이 명세대로 동작한다는 증명을 함께 쓰게 하는 정적 타입 언어입니다. 저자 훙웨이 시는 기본 함수형 프로그래밍부터 의존 타입(값에 따라 정해지는 타입)과 선형 타입(자원을 정확히 한 번만 쓰게 하는 타입)까지 차례로 다룹니다.
왜 중요한가
- 구현이 명세에서 멀어져 유지보수가 위험해지는 문제를 언어 차원에서 막으려는 시도입니다.
- 구현자가 증명까지 직접 쓰는 '프로그래머 중심 검증'을 이론보다 실제 코드로 보여 줍니다.
핵심 내용
- ATS는 타입과 명세를 다루는 정적 부분, 구현을 다루는 동적 부분, 정리 증명 시스템으로 이뤄집니다.
- 수학의 기초를 세우려고 만든 마르틴뢰프의 구성적 타입 이론에서 큰 영향을 받았습니다.
- 책은 5부 17장으로, 함수형 기초부터 C 연동, 의존 타입, 뷰타입, 함수 템플릿까지 다룹니다.
- 언어의 핵심은 값에 의한 호출(call-by-value) 방식의 단순한 함수형 언어입니다.
- 프로그래밍 경험이 없어도 된다고 하지만, 경험이 적으면 꽤 빽빽하게 느껴질 수 있다고 밝힙니다.
HN 반응
- ATS2(Postiats)는 몇 년째 사실상 동결됐고, 후속작 ATS3(Xanadu)는 아직 실제로 쓰기 어렵다는 설명이 나왔습니다.
- ATS3은 ML식 타입 검사 위에 의존 타입을 얹어 진입 장벽을 낮추려 한다는 보충과 함께, 릴리스 노트가 없어 현황을 알기 어렵다는 아쉬움도 있었습니다.
ATS는 예전에 HN에서 꽤 자주 거론되던 주제였습니다.
https://hn.algolia.com/?query=The%20ATS%20Programming%20Language&type=story&dateRange=all&sort=byDate&storyText=false&prefix&page=0
MLton과 Felix도 ML에서 영감을 받은 언어로, 프로그램 전체를 최적화해서 빠른 코드를 만들어 냅니다.
http://www.mlton.org/
https://felix.readthedocs.io/en/latest/
저는 제가 만들고 있는 프로그래밍 언어에 MLton에서 영감을 많이 얻었습니다. ATS에서도 영감을 얻고 싶은데, 그쪽은 좀 더 복잡해서요. 앞으로 나아갈 방향을 가리키는 북극성쯤으로 마음에 품고 있습니다.
언어를 설계할 때 더 많은 사람이 이런 언어들을 알아보면 좋겠습니다. LLM이 딥 리서치에서 이런 언어를 짚어 주는 데 도움이 되기는 하지만, 사람이 그 방향으로 생각하고 있을 때 얘기입니다.
이 언어를 다룬 재미있는 발표가 있습니다. https://www.youtube.com/watch?v=zt0OQb1DBko (Aditya Siram의 "A (Not So Gentle) Introduction To Systems Programming In ATS")
흥미로워 보입니다. 활발히 개발되고 있네요. https://github.com/githwxi/ATS-Postiats
수정: 맞는 말씀입니다. 세 번째 버전이 있는 줄 몰랐습니다. 릴리스 노트라도 있으면 좋을 텐데요. 지금 이 언어가 어떤 상태인지 전혀 모르겠습니다. Hongwei, 보고 계시다면 부탁드립니다!
이 언어가 뭔가 되려면 커뮤니티 차원의 개발이 필요합니다.
커밋 메시지가 전부 "very very minorly"뿐이라 따라가기가 "아주 아주 조금" 어렵긴 한데, 제가 보기에 ATS2(Postiats)는 유지보수 모드이고(최근 활동은 빌드 관련 변경입니다) 활발한 개발은 ATS3(Xanadu)에 집중되어 있는 것 같습니다. https://github.com/githwxi/ATS-Xanadu
ATS2는 몇 년째 사실상 동결 상태입니다. 최근 커밋은 대부분 ATS3를 컴파일할 수 있게 하려는 빌드 변경입니다. ATS2는 안정적이라 지금 당장 쓸 수 있고, 릴리스 노트는 저장소의 CHANGES-ats2에 있습니다. 제 블로그(https://bluishcoder.co.nz/tags/ats/)에 ATS2와 이전 버전인 ATS1의 기능을 보여 주는 글이 몇 편 있습니다. ATS3는 개발 중입니다. 자기 자신을 컴파일하긴 하지만, 제가 보기에 아직은 일반적으로 쓸 만한 수준이 아닙니다. 설계상 가장 큰 변화는 2계층 타입 검사입니다. 먼저 ML 스타일로 검사하고 그 위에 의존 타입을 얹어서, 학습 곡선을 낮추려는 시도입니다. 진행 상황을 따라가기에는 ats-lang-users 구글 그룹이 가장 좋을 겁니다.
Abstract Tree Syntax(추상 트리 구문)요.
Applicant Tracking System(지원자 추적 시스템)이죠.
Are They Serious?(지금 진심이에요?)