Quint의 최고경영자(CEO) 가브리엘라 모레이라(Gabriela Moreira)는 AI의 도움으로 새 코드베이스의 테스트가 약 200개에서 800개로 늘었지만, 테스트를 덜 신뢰하게 됐고 동작을 직접 확인하는 일이 많아졌다고 말했다. 모레이라는 테스트 개수보다 테스트가 어떤 동작을 보호하는지 이해하는 일이 중요하다고 설명하며, 소프트웨어 동작을 모델링하고 검증하는 오픈소스 명세 언어 Quint를 소개했다.
Quint는 TLA+의 영향을 받은 실행 가능한 명세 언어다. 개발자는 이를 이용해 여러 사용자가 얽힌 상황이나 상태 변화, 동시성처럼 가능한 동작이 많아 머릿속으로 모두 따지기 어려운 사례를 모델링하고, 문제가 실제 서비스에 나타나기 전에 예외 상황을 탐색할 수 있다. 모레이라는 형식 명세가 은행이나 안전 필수 시스템에만 필요한 것은 아니라고 주장했다.
대화에서는 모델 기반 테스트와 실행 추적 검증, 명세와 실제 코드의 동기화를 유지하는 어려움도 다뤘다. 모레이라는 OpenHands 팀이 Kubernetes의 간헐적 경쟁 상태를 Quint로 모델링한 사례를 소개했다. 분석 결과 처음 제안된 수정안은 다른 시나리오에서 여전히 실패할 수 있었고, 팀은 운영 환경에서 문제가 다시 발생하기 전에 다른 해결책을 탐색할 수 있었다.
모레이라는 AI가 구현과 디버깅을 더 많이 맡게 될수록 소프트웨어가 어떻게 동작해야 하는지 판단하는 능력이 중요해진다고 말했다. 에이전트에게 넘기기 전에 해결책을 거대한 마크다운 문서로 빠짐없이 설명하는 방식에는 회의적이다. 직접 시도하고 결과를 살피며 이해를 바꾸는 탐색 과정도 프로그래밍의 중요한 부분이며, AI가 반복 작업을 맡더라도 사람의 평가와 판단은 필요하다는 설명이다.
Quint와 관련 자료는 Quint, Quint GitHub 저장소, TLA+, Quint 시작 가이드에서 확인할 수 있다. 사례와 배경 자료로는 OpenHands의 Kubernetes 사례, 인지 부채에 관한 글, Quint Connect와 Emerald 프로젝트, 패트릭 로스퍼스의 소설 《바람의 이름》이 소개됐다.
댓글 (0)
로그인하면 이 기사에 내 생각을 남길 수 있어요