제인스트리트, 형식 검증 방법 도입으로 전환
원제: Formal methods and the future of programming
왜 중요한가
AI 코딩 시대에 형식 검증이 코드 품질 보장의 핵심 도구로 부상할 가능성을 시사한다.
금융 거래회사 제인스트리트가 25년간 거부해온 형식 검증 방법(formal methods) 도입을 선언했다. AI 에이전트 코딩의 등장으로 비용 대비 효과가 개선되어 전담 팀을 구성한다고 발표했다.
제인스트리트의 야론 민스키(Yaron Minsky)는 회사가 25년간 형식 검증 방법에 회의적이었다가 AI 에이전트 코딩의 등장으로 입장을 바꿨다고 밝혔다. 기존에는 형식 검증의 비용이 너무 높았는데, seL4 마이크로커널 사례를 보면 8,700줄의 C 코드 검증에 25인년이 소요되고 코드 한 줄당 23줄의 증명과 0.5인일이 필요했다.
하지만 AI 에이전트가 형식 검증 방법의 비용 구조를 극적으로 변화시켰다. 모델이 증명 구성에 도움을 주고 더 많은 사람이 이런 도구를 생산적으로 사용할 수 있게 됐다. 또한 AI가 생성한 코드는 유용하지만 품질 검증이 필요한데, 형식 검증이 이런 검토 부담을 덜어줄 수 있다. AI 에이전트는 피드백을 통해 성능이 향상되는 특성도 있어 형식 검증과의 시너지 효과가 기대된다.
제인스트리트는 형식 검증 방법을 현재의 정교한 타입 시스템처럼 소프트웨어 구축의 보편적 도구로 만드는 것을 목표로 전담 팀을 구성한다고 발표했다.