본 노트는 The Pragmatic Engineer 뉴스레터(유료 구독 콘텐츠)의 핵심 내용을 정리한 요약 노트입니다. 저작권 보호를 받는 원문 전문을 그대로 옮기는 대신, 주요 논지와 사례를 빠짐없이 우리말로 재구성했습니다. 전체 원문과 트랜스크립트는 위 원문 링크에서 확인할 수 있습니다.
에피소드 소개
AI가 코드 대부분을 작성하게 되면 결국 수학적 정합성 증명, 즉 형식 검증(formal verification)이 주류가 될 것이라는 예측이 있다. 이 에피소드에서 진행자는 형식 방법(formal methods) 컨설턴트이자 교육자, 저자인 Hillel Wayne과 이 예측을 검증한다. 소프트웨어 엔지니어링과 전통적인 엔지니어링의 차이, 형식 방법이 현대 개발에서 차지하는 위치, TLA+를 비롯한 여러 형식 검증 도구, 분산 시스템을 추론하기 어려운 이유, 그리고 AI가 형식 방법을 더 대중화할 수 있을지를 다룬다.
대화에서 얻은 핵심 내용
1. 소프트웨어 엔지니어는 "진짜" 엔지니어인가 Hillel은 자신의 Crossover Project를 위해 전통 공학과 소프트웨어 공학 각 분야에서 약 20명을 인터뷰했다. 두 분야 사이에는 유사점과 차이점이 공존했지만, 결론적으로 소프트웨어 엔지니어링이 요구하는 엄격함 자체가 "엔지니어"라는 명칭을 정당화한다고 봤다.
2. 버전 관리는 소프트웨어 엔지니어링의 독자적 강점 다른 공학 분야에도 변경 관리 개념은 있지만, 소프트웨어의 버전 관리만큼 정교하지 않다. 전통 엔지니어들이 오히려 이를 부러워한다.
3. TLA+란 무엇인가 Leslie Lamport(LaTeX 창시자이자 수학자)가 복잡한 시스템을 모델링하기 위해 만든 형식 명세 언어. 시스템을 상태 기계로 표현하고, 초기 상태에서 도달 가능한 모든 상태를 열거한 뒤, 사전에 정의한 속성이 그 모든 상태에서 성립하는지 검사한다. Hillel은 에피소드 중 실제 데모로 이를 보여준다.
4. Amazon이 TLA+로 찾아낸 버그 "How AWS uses formal methods" 논문에 따르면, AWS는 오류를 재현하는 최단 경로가 35단계에 달하는 버그를 TLA+로 발견했다. 이 버그는 설계 리뷰, 코드 리뷰, 일반 테스트를 모두 통과했을 정도로 은밀했으며, 기존 테스트 방식만으로는 절대 발견하지 못했을 것이라는 게 AWS의 결론이었다.
5. 동시성/경쟁 조건에 약한 이유는 연습 부족 경쟁 조건(race condition) 버그는 보통 몇 달 뒤에야, 혹은 영영 발견되지 않는다. 반면 TLA+로 모델링하면 도구 실행 즉시 경쟁 조건을 알려줘 피드백 루프가 훨씬 빠르다.
6. 왜 모든 곳에 형식 검증을 쓰지 않는가 현실의 스펙 작성 자체가 지옥이기 때문이다. "디렉터리에서 줄 수가 가장 많은 파일 찾기"처럼 단순해 보이는 문제도 형식화하려면 개행 문자 인코딩, 읽기 불가능한 파일, 심볼릭 링크 처리 등 온갖 예외를 정의해야 한다. 형식 방법 없이도 99% 이상의 경우에 맞는 검증은 쉽게 짤 수 있지만, 나머지 1% 미만의 예외적 케이스를 위해 형식 방법은 막대한 추가 노력을 요구한다.
7. Hillel의 실용적 권고: 속성 기반 테스트(property-based testing) 대부분의 엔지니어에게는 형식 방법보다 속성 기반 테스트가 현실적이다. 지켜야 할 속성을 정의하면 테스트 도구가 수천 개의 입력값으로 시스템을 스트레스 테스트한다. Hillel은 형식 방법을 소수 전문가를 위한 틈새 도구로, 속성 기반 테스트를 가벼우면서도 실용적인 대안으로 본다.
8. AI는 형식 검증을 대중화하지 못하지만 사용량은 늘릴 것 Hillel: "AI가 업계 전체 형식 검증 사용률을 0.1%에서 0.3%로만 끌어올려도 엄청난 변화다." 다만 AI로 형식 명세를 성공적으로 생성하는 사람들은 대개 이미 형식 검증 전문가인 경우가 많다는 점도 지적한다.
9. Time-of-check to time-of-use 버그 "확인하는 시점"(예: 계좌 잔액 확인)과 "실행하는 시점"(예: 실제 출금) 사이에 시간 간격이 생기는 이 버그 유형은 방어하기 까다롭고 실제 시스템에서 골치 아픈 문제를 일으킨다. Hillel이 특히 신경 쓰는 취약점이다.
10. AI로 인한 걱정은 실업보다 "직업의 평범화" 2025년 AI 영향 예측을 다시 짚으며, Hillel은 미래의 소프트웨어 엔지니어링이 지금보다 낮은 임금과 낮은 위상을 갖게 될 가능성을 우려한다. 지금은 전통 공학 대비 커리어 선택지가 유독 풍부하지만, 이 특권이 계속될지는 미지수다.
11. 가장 인상 깊었던 프로젝트: 열차 트랜스폰더 검증 데이터베이스나 분산 시스템 이외에도 디바이스 펌웨어를 형식 검증한 경험이 있다. 철로 사이에서 제어 시스템으로 정보를 전달하는 전자 비콘 프로젝트에서 이상한 버그를 발견했고, 이를 고쳐 실제 철도 시스템의 신뢰성과 안전성을 높였다.
12. 소프트웨어가 전통 공학에서 배울 점: "기본기" 서적 문화 Hillel이 좋아하는 책 중 하나는 배터리 커버를 고정하는 작은 클립만 다루는 500쪽짜리 The First Snap-Fit Handbook이다. 다른 산업은 사소해 보이는 주제조차 방대하게 문서화하는데, 소프트웨어 엔지니어링에는 API 버전 관리법 하나 제대로 다룬 책도 없다. 여기서 배울 점이 있다는 지적이다.
13. 소프트웨어의 "재료"는 이상할 정도로 일관적 전기 엔지니어는 1,000개 저항기 중 특정 온도 범위 안에서 100옴의 ±20% 오차를 감수해야 하는 등 재료의 변동성과 늘 싸운다. 반면 소프트웨어는 어떤 컴퓨터에서도 동일하게 실행된다. Hillel은 소프트웨어에서 겪는 버전 호환성, API 불일치, 통합 버그 같은 "변동성"은 사실 대부분 우리가 스스로 만들어낸 문제라고 짚는다.
함께 보면 좋은 The Pragmatic Engineer 딥다이브
- 대규모 분산 시스템 디버깅: Antithesis
- AWS S3는 어떻게 만들어졌는가
- 기술 부채 상환하기
- 빅테크의 QA 방식
- 효과적인 버그 관리
- 분산 시스템의 복원력(Resiliency)
주요 타임스탬프
- 04:32 Crossover Project
- 18:17 형식 방법
- 29:32 TLA+ 개념과 데모
- 36:58 Amazon에서의 TLA+
- 41:03 형식 방법과 시스템 사고
- 52:50 Alloy (선언형 모델링 언어)
- 1:01:24 속성 기반 테스트
- 1:05:31 AI와 형식 검증의 필요성
- 1:21:30 도서 추천
참고 링크
- Hillel Wayne 웹사이트: https://www.hillelwayne.com
- Hillel Wayne 뉴스레터: https://buttondown.com/hillelwayne
- TLA+: https://github.com/tlaplus
- Use of Formal Methods at Amazon Web Services (PDF): https://lamport.azurewebsites.net/tla/formal-methods-amazon.pdf
- Alloy: https://alloytools.org
- Time-of-check to time-of-use (Wikipedia): https://en.wikipedia.org/wiki/Time-of-check_to_time-of-use
- Logic for Programmers: https://leanpub.com/logic
- P (분산 시스템 형식 모델링): https://github.com/p-org/P
- Quint: https://quint.sh
- Dafny: https://dafny.org
핵심 요약 (20줄)
- AI가 코드 대부분을 작성하는 시대가 오면 형식 검증이 주류가 될 것이라는 예측을 형식 방법 전문가 Hillel Wayne과 함께 검증한다.
- Hillel은 Crossover Project에서 약 20명을 인터뷰한 끝에, 소프트웨어 엔지니어링에 필요한 엄격함이 "엔지니어"라는 이름값을 정당화한다고 결론지었다.
- 소프트웨어의 버전 관리 시스템은 다른 공학 분야보다 훨씬 정교해서, 전통 엔지니어들이 부러워하는 대상이다.
- TLA+는 Leslie Lamport가 만든 형식 명세 언어로, 시스템을 상태 기계로 표현해 도달 가능한 모든 상태에서 속성이 성립하는지 검사한다.
- AWS는 TLA+로 오류 재현에 35단계가 필요한, 기존 테스트로는 발견 불가능했던 버그를 찾아냈다.
- 경쟁 조건(race condition) 버그는 보통 뒤늦게 발견되지만, TLA+ 모델은 즉시 이를 알려줘 피드백 루프가 훨씬 빠르다.
- 형식 방법을 모든 곳에 쓰지 않는 이유는 현실 스펙 작성이 지나치게 복잡해지기 때문이다 → 단순한 문제도 온갖 예외 조건을 요구한다.
- 형식 방법 없이도 99% 이상의 케이스는 간단히 검증 가능하며, 나머지 1% 미만을 위해 형식 방법은 막대한 추가 비용을 요구한다.
- Hillel은 대부분의 엔지니어에게 형식 방법 대신 속성 기반 테스트(property-based testing)를 권한다.
- 속성 기반 테스트는 정의한 속성에 대해 수천 개의 입력값을 자동으로 던져 시스템을 검증하는 실용적 경량 형식 방법이다.
- AI는 형식 검증을 주류로 만들지는 못하지만 사용률을 0.1%에서 0.3%로만 올려도 산업 전체에 큰 임팩트가 있다.
- AI로 형식 명세 생성에 성공하는 사람들은 대부분 이미 형식 검증 전문가라는 점이 흥미로운 관찰이다.
- Time-of-check to time-of-use 버그(확인 시점과 실행 시점의 간격)는 Hillel이 특히 우려하는, 방어하기 어려운 버그 유형이다.
- Hillel은 AI로 인한 실업보다 소프트웨어 엔지니어링 직업 자체가 "평범한 직업"으로 격하될 가능성을 더 걱정한다.
- 열차 트랙 사이 전자 비콘의 트랜스폰더 펌웨어를 형식 검증해 이상한 버그를 찾아내고 철도 시스템의 안전성을 높인 경험이 인상적인 사례로 소개된다.
- 소프트웨어 업계에는 배터리 커버 클립만 다룬 500쪽짜리 책 같은 "기본기" 문서 문화가 부족하다 → API 버전 관리법을 제대로 다룬 책조차 없다.
- 전기 엔지니어는 부품의 물리적 오차 범위와 늘 싸워야 하지만, 소프트웨어는 어떤 컴퓨터에서든 동일하게 실행되는 이상할 정도의 일관성을 가진다.
- Hillel은 소프트웨어에서 겪는 버전·API·통합 버그 같은 변동성은 대부분 우리 스스로 만든 문제라고 지적한다.
- 에피소드에서는 TLA+ 데모 외에도 Alloy, P, Quint, PRISM, NuSMV, Dafny, JML, Frama-C, Ada SPARK 등 다양한 형식 검증 도구가 비교 소개된다.
- 결론적으로 형식 방법은 만능이 아니라, 고위험·고복잡도 시스템에 선택적으로 적용해야 할 전문 도구이며, 대다수 엔지니어에게는 속성 기반 테스트가 더 실용적인 대안이다.