사양은 존재하지 않는다

Specifications Don't Exist (2025)

갤로이스(Galois)의 마이크 도즈(Mike Dodds)는 공식 검증(formal verification)의 성공 사례가 컴파일러, 암호화 라이브러리, 마이크로커널 등 자연적으로 형식화 가능한 시스템에 국한되어 있다고 주장합니다. 그러나 대부분의 실제 시스템, 예를 들어 웹 브라우저나 PDF 같은 것은 명확한 경계가 없어 정확하고 일관된 공식 사양을 작성하는 것이 불가능하다고 설명합니다. 그는 PDF를 예로 들어, 실제 구현들이 비표준 문서를 관대하게 처리하면서 'PDF'라는 범주 자체가 모호해졌다고 분석합니다. 결론적으로, AI가 증명 비용을 낮추더라도 '무엇을 원하는지'를 명시하는 사양 작성이 여전히 가장 큰 난관이라고 강조합니다.