Write down every guarantee before you write any code

개요

코드 작성 전에 모든 보장 사항을 명확히 정의하는 것이 중요하다는 점을 강조하며, 이를 위해 TLA+와 같은 형식 기법을 사용하여 시스템의 동작 규칙을 명시하고, 이를 생성된 코드와 대조하여 검증하는 방법을 제시합니다.

주요 내용

* 보장 사항의 명시: To-do 리스트와 같은 간단한 기능도 변수(tasks), 초기 상태(Init), 동작(Add, Complete, Reopen, Delete, ClearCompleted)에 대한 엄격한 정의를 통해 모든 보장 사항을 명확하게 명시할 수 있습니다.
* TLA+를 활용한 명세: Spec == Init /\ [][Next]_tasks와 같은 TLA+ 사양은 시스템이 합법적으로 시작하고 항상 합법적인 상태 변화만 발생함을 나타내며, 이는 데이터베이스나 HTTP와 같은 구현 세부 사항을 제외한 순수한 규칙 집합입니다.
* 명세 작성의 이점:
* 조기 버그 발견: 코드가 작성되기 전에 디자인 단계에서 설계상의 버그를 발견할 수 있습니다. AWS의 경험에 따르면, 이미 설계되고 검토된 시스템에서도 명세를 작성하는 과정에서 버그가 발견되었습니다.
* 협업 효율 증대: 엔지니어 간의 동작 규칙에 대한 불일치가 코드 리뷰나 긴 논쟁 대신 짧은 시간 안에 명확하게 해결될 수 있습니다.
* 실행 가능한 보장: 명세는 단순한 문서가 아니라, 검증 도구를 통해 실제 구현과 비교 검증할 수 있는 실행 가능한 보장 사항이 됩니다.
* 자동화된 검증 도구 (tlatools-rs):
* tlatools-rs는 TLA+ 파서 및 평가기로, 주어진 상태에 대한 명세의 유효성을 검사하고, 특정 상태에서 다음 상태로의 전이가 명세에 허용되는지 확인할 수 있습니다.
* 이 도구를 사용하여 구현체가 명세에 정의된 규칙을 따르는지 기계적으로 검증할 수 있으며, 이는 코드 생성기, 모델 평가, 벤치마크 채점 등에 활용될 수 있습니다.
* tlatools check 명령을 통해 JSON 형식의 작업 파일을 입력받아 명세와의 일치 여부를 판단하고, 불일치 시 상세한 정보를 제공합니다.
* AI 코드 생성 시의 중요성: AI가 코드를 생성하는 시대에는 AI가 시스템의 규칙을 이해하지 못하므로, 명확하게 작성된 명세와 이를 검증하는 메커니즘이 더욱 중요해집니다. AI가 생성한 그럴듯한 코드도 명세에 기반하여 기계적으로 검증해야 합니다.
* 검증 도구의 한계 및 신뢰성:
* tlatools-rs는 모델 체커가 아니므로 도달 가능한 모든 상태를 탐색하지는 않으며, 단지 주어진 트랜지션이 명세에 허용되는지를 확인합니다.
* 검증 도구는 명세의 정확성에 의존하며, 명세 자체가 잘못 작성되었다면 검증 결과도 오해를 불러일으킬 수 있습니다.
* tlatools-rs는 Java TLC와 동일한 결과를 제공하며, TLA+ 파일의 상당 부분을 오류 없이 읽을 수 있음을 보여줍니다.
* 적용 및 시작 방법: 시스템에서 잘못된 상태 변경이 치명적인 부분(금전, 권한 등)을 선택하고, 해당 부분의 허용되는 동작들을 정의하는 것으로 시작할 수 있습니다.

시사점

시스템의 모든 보장 사항을 명확하게 문서화하고 기계적으로 검증하는 과정을 통해, 코드 작성 전 단계에서부터 오류를 방지하고 시스템의 신뢰성을 높일 수 있으며, 이는 AI 코드 생성 시대에도 필수적인 개발 방법론이 될 것입니다.