Vera: 사람이 아닌 AI 모델을 위해 설계된 프로그래밍 언어

이 요약은 AI가 원문을 분석해 생성했습니다. 정확한 내용은 원문 기준으로 확인하세요.

핵심 요약

AI 모델이 코드를 생성할 때 발생하는 일관성 결여와 오류를 해결하기 위해 변수명을 없애고 Z3 SMT 솔버로 논리적 계약을 강제하는 기계 중심 프로그래밍 언어 Vera를 소개합니다.

배경

AI 모델의 코딩 능력이 향상되고 있지만 대규모 시스템의 일관성 유지에는 여전히 한계가 있습니다. 작성자는 모델이 정확할 필요 없이 컴파일러를 통해 검증 가능하도록 설계된 오픈소스 언어 Vera를 개발하여 공유했습니다.

의미 / 영향

이 프로젝트는 프로그래밍 언어 설계의 패러다임이 인간의 가독성에서 기계의 검증 가능성으로 이동할 수 있음을 시사합니다. 향후 AI 에이전트가 소프트웨어 개발의 주류가 될 때 인간 중심의 문법보다 기계적 엄밀함을 강조하는 전용 언어의 필요성이 더욱 커질 것입니다.

커뮤니티 반응

작성자는 인프라 구축을 완료하고 1,287개의 테스트를 통과시켰으나, 실제 모델이 기존 언어보다 Vera에서 더 신뢰할 수 있는 코드를 생성하는지에 대한 체계적인 데이터는 아직 부족하다고 밝히며 커뮤니티의 실험을 독려하고 있습니다.

주요 논점

01중립다수

AI 코딩의 핵심 지표는 유창성(Fluency)이 아니라 검증을 통한 신뢰성(Reliability)이 되어야 합니다.

합의점 vs 논쟁점

합의점

AI 모델은 대규모 코드베이스에서 불변성을 유지하고 변경의 파급 효과를 이해하는 데 어려움을 겪습니다.
현재 AI 코딩의 발전은 모델 자체보다 모델을 보조하는 워크플로우의 개선에서 크게 나타나고 있습니다.

실용적 조언

AI 에이전트를 설계할 때 모델에게 자유로운 작성을 맡기기보다 엄격한 타입 시스템과 논리 검증기를 갖춘 환경을 제공하는 것이 유리합니다.
모델에게 제공하는 에러 메시지는 단순한 상태 표시가 아니라 구체적인 수정 방법과 예시 코드를 포함한 지침 형태여야 합니다.

언급된 도구

Vera추천링크

AI 모델 전용 프로그래밍 언어 및 컴파일러

Z3 SMT Solver추천

함수 계약 및 논리적 제약 조건 검증

Wasmtime중립

WebAssembly 컴파일 및 실행 환경

섹션별 상세

AI 모델의 코딩 성과는 모델 자체의 지능보다 이를 둘러싼 에이전틱 루프(Agentic loops)와 피드백 시스템의 발전에 더 큰 영향을 받습니다. 린터나 테스트 러너가 제공하는 구조화된 피드백 덕분에 모델은 한 번에 완벽한 코드를 짜는 대신 반복적인 수정을 통해 품질을 높일 수 있게 되었습니다. Vera는 이러한 관찰을 바탕으로 모델과 환경 사이의 피드백 루프를 극대화할 수 있도록 설계된 언어입니다. 즉, 모델이 환경과 상호작용하며 스스로 오류를 바로잡을 수 있는 최적의 구조를 제공하는 것이 핵심 목적입니다.

인간 개발자에게 필수적인 변수 이름을 과감히 제거하고 타입이 지정된 드 브루인 인덱스(De Bruijn indices)를 사용하여 구조적 참조 방식을 채택했습니다. 이는 모델이 변수 이름을 잘못 지어 발생하는 명명 일관성 오류를 근본적으로 차단하며, 잘못된 인덱스 사용 시 타입 시스템이 이를 기계적으로 즉각 포착하게 합니다. 결과적으로 모델은 이름 매칭이라는 모호한 작업 대신 코드의 논리적 구조와 타입 일치에만 집중하여 코드를 작성할 수 있습니다.

모든 함수에 전제 조건, 사후 조건, 효과를 명시하는 계약(Contract) 작성을 의무화하고 이를 Z3 SMT 솔버를 통해 검증합니다. 예를 들어 0으로 나누는 행위는 런타임 에러가 아닌 타입 에러로 처리되어 모델이 모든 엣지 케이스를 기억할 필요 없이 컴파일러가 논리적 의무를 강제합니다. 이러한 설계는 모델이 논리적으로 완벽해야 한다는 부담을 덜어주는 대신 컴파일러가 제시하는 제약 조건을 충족하도록 유도하여 코드의 신뢰성을 보장합니다.

컴파일러의 진단 메시지는 모델이 즉시 이해하고 수정할 수 있도록 자연어 수정 지침과 구체적인 코드 예시를 포함하도록 구조화되었습니다. 이는 작성-검사-수정으로 이어지는 에이전트 기반 코드 생성 루프를 완성하는 핵심 요소로 작용합니다. 또한 모델의 컨텍스트 윈도우에 직접 삽입할 수 있는 전용 문서를 제공하여 모델이 학습 데이터의 기억에 의존하지 않고 실시간 명세를 바탕으로 정확하게 동작하도록 돕습니다.

실무 Takeaway

AI 모델의 코딩 성능 향상은 모델 지능보다 에이전틱 루프와 피드백 도구의 발전에서 기인합니다.
Vera는 변수명을 없애고 구조적 참조를 도입하여 모델의 명명 오류와 일관성 문제를 해결합니다.
Z3 SMT 솔버를 활용한 강제적 함수 계약을 통해 런타임 오류를 컴파일 단계의 논리 검증으로 전환합니다.
모델이 유창하게 코드를 쓰는 것보다 컴파일러를 통해 검증 가능함을 보장받는 것이 안정적인 코드 생성의 핵심입니다.

언급된 리소스

GitHubVera GitHub Repository

문서A language designed for machines to write