타입 검사도 통과, 테스트도 통과 — 그런데 왜 순서 때문에 깨질까? 개발자를 위한 TLA+ 입문
한 줄 요약
수학자에게 증명을 검사해 주는 Lean이 있다면, 개발자에게는 동시성 설계를 명세하고 검증하는 **TLA+**와 모델 검사기 TLC가 있습니다. 배포 후에야 사용자가 찾아내던 논리의 허점을, 배포 전에 기계의 힘으로 먼저 찾아보자는 이야기입니다.
우리는 사실 '런타임으로 증명'하고 있었다
거칠게 말하면 프로그래밍은 이런 일입니다.
내가 만든 논리가 틀리지 않았는지, 사용자에게 배포해서 런타임 실행으로 증명하는 일
조금 서늘한 문장입니다. 검증의 마지막 단계를 사용자에게 떠넘기고 있다는 뜻이니까요. 그렇다면 질문은 자연스럽게 이어집니다. 배포 전에 더 많이 찾아낼 수는 없을까요?
증명과 타입 검사는 생각보다 가깝다
힌트는 이미 우리 손에 있습니다. 수학의 증명과 프로그래밍의 타입 검사는 멀리 떨어진 세계가 아닙니다.
커리–하워드 대응(Curry–Howard correspondence) 은 이렇게 말합니다.
- 명제(proposition) → 타입
- 증명(proof) → 그 타입을 가진 프로그램
즉 증명을 구성하고 검사하는 일은, 프로그램을 작성하고 타입을 검사하는 일과 구조적으로 연결되어 있습니다. 수학자들이 Lean으로 증명을 기계 검사하듯, 개발자도 자신의 설계를 기계에 검사시킬 수 있다는 발상이 여기서 출발합니다.
그런데 타입 검사가 잡지 못하는 것: 순서
문제는 여기서 시작됩니다.
- 타입 검사 통과 ✅
- 유닛 테스트 통과 ✅
- 그런데 A가 B보다 먼저 끝났다는 이유만으로 프로그램이 깨짐 ❌
동시성 버그의 전형적인 모습입니다. 상태(state)는 어떻게든 눈으로 훑어볼 수 있지만, 순서(ordering) 는 그렇지 않습니다. 숫자로 보면 더 명확합니다.
각각 내부 순서를 지키는 10단계짜리 작업 두 개를 섞어 실행하는 경우의 수 = 184,756가지
사람이 고른 몇 개의 테스트 케이스로 이 공간을 덮는 건 사실상 불가능합니다. 상태보다 어려운 것은 순서입니다.
TLA+와 TLC가 하는 일
TLA+는 시스템의 동작을 명세(specification) 로 적는 언어이고, TLC는 그 명세를 검사하는 모델 검사기입니다. 핵심 차이는 이것입니다.
| | 유닛 테스트 | TLC 모델 검사 | |---|---|---| | 탐색 범위 | 내가 고른 케이스 | 유한 모델이 허용하는 모든 실행 | | 결과 | 통과/실패 | 조건을 깨뜨리는 반례(counterexample) |
TLC는 "이 케이스는 어떤가요?"라고 묻지 않습니다. 설정한 유한 모델 안에서 가능한 실행들을 훑으며, 내가 세운 조건을 깨뜨리는 시나리오를 직접 찾아옵니다.
실전 예시: RxJS의 공유 연결 문제
원문에는 아주 현실적인 사례가 등장합니다.
- 여러 작업이 하나의 연결(connection)을 공유하는 RxJS 코드
- 먼저 끝난 작업이 다른 작업도 쓰고 있는 공유 연결까지 닫아버리는 문제
이 상황을 작은 TLA+ 명세로 옮기고, 검사할 조건을 이렇게 세웁니다.
작업이 하나라도 실행 중이면, 연결은 열려 있어야 한다
이 한 줄이 바로 불변식(invariant)입니다. 원문은 여기에 더해 TLC 검사 설정과 실행 명령까지 함께 제시합니다. 거창한 형식 검증 프로젝트가 아니라, 버그 하나를 재현하는 작은 모델 수준이라는 점이 중요합니다.
AI가 바꾸는 비용 구조
그동안 TDD와 유닛 테스트에는 늘 그림자가 따라다녔습니다. 작성 비용과 유지 비용입니다. 형식 명세는 그 비용이 훨씬 더 컸고요.
그런데 지금은 상황이 달라지고 있습니다.
- AI는 테스트 초안을 만드는 비용을 크게 낮췄습니다
- 같은 방식으로 상태 모델과 검사 조건의 초안도 만들 수 있습니다
진입 장벽의 상당 부분이 "문법과 초기 작성"이었다면, 그 장벽은 눈에 띄게 낮아진 셈입니다.
다음 '공짜 점심'은 동시성 검증
원문의 제안은 명료합니다.
- 개발자를 가장 오래 괴롭혀 온 문제 중 하나는 병렬·비동기 실행 순서
- 유닛 테스트를 하나 추가하듯, 작은 TLA+ 모델을 하나 추가해 보자
- 사용자가 아니라 배포 전의 내가 반례를 먼저 만나자
전체 시스템을 형식 명세로 옮기라는 이야기가 아닙니다. 의심스러운 동시성 지점 하나를 골라, 지켜야 할 조건 한 줄을 적고, TLC를 돌려보는 것부터 시작하면 됩니다.
마치며
타입 검사는 "이 값이 말이 되는가"를 지켜줍니다. 하지만 "이 일들이 이 순서로 일어나도 말이 되는가"는 지켜주지 않습니다. 그 빈칸을 메우는 도구가 이미 수십 년 전부터 있었고, 이제는 AI 덕분에 손을 뻗기가 한결 수월해졌습니다.
다음에 재현되지 않는 동시성 버그를 만난다면, 로그를 한 줄 더 찍기 전에 작은 명세를 하나 적어보는 건 어떨까요?