LLM을 위한 논리 검증형 프로그래밍 언어 'Brief' 공개

실용적 조언

LLM을 활용한 코딩 시 언어 자체의 제약 조건이 강할수록 모델의 할루시네이션을 억제하는 데 도움이 된다.
복잡한 상태 관리가 필요한 프로젝트에서는 선언형 상태 매핑을 도입하여 버그 발생 가능성을 낮출 수 있다.

섹션별 상세

LLM은 TypeScript나 JavaScript 작성 시 상태 변화 로직에서 빈번하게 실수를 저지르며 이는 런타임 에러로 이어진다. Brief는 이를 해결하기 위해 모든 함수 호출에 전제 조건(Precondition)과 사후 조건(Postcondition)을 선언하는 Hoare triple 구조를 도입했다. 컴파일러가 실행 전 논리적 부합 여부를 검증하므로 LLM이 생성한 코드의 결함을 즉시 포착하는 효과가 확인됐다.

text

let counter: Int = 0;
let ready: Bool = false;

// Passive transaction
txn initialize [~/ready] {
  &ready = true;
  term;
};

// Reactive transaction
rct txn increment [ready && counter < 4] {
  &counter = counter + 1;
  term;
};

전제 조건과 사후 조건을 활용한 Brief 언어의 트랜잭션 정의 예시

명령형 방식 대신 선언형 논리 엔진 방식을 채택하여 프로그램의 모든 상태 변화를 추적 가능하게 설계했다. 특정 시점에 무엇이 참이고 거짓인지 논리적으로 추론할 수 있어 단순한 스택 트레이스 대신 어떤 논리가 왜 성립하지 않는지에 대한 직접적인 피드백을 제공한다. 이는 복잡한 분기 처리가 필요한 시스템에서 상태 불일치 문제를 원천 차단하는 장점이 있다.

text

rstruct Counter {
  count: Int;
  txn Counter.increment [true][@count + 1 == count] {
    &count = count + 1;
    term;
  };
  // ...
  <div>
    <h1>Counter: {count}</h1>
    <button onclick={Counter.increment}>+</button>
  </div>
}

로직과 HTML/CSS가 결합된 Rendered Brief의 컴포넌트 구조

외부 세계와의 상호작용은 Foreign 함수로 분류하여 기본적으로 신뢰하지 않는 상태로 취급한다. TOML 파일을 통해 외부 언어의 입출력을 Brief의 계약과 매핑하며 모든 리턴 케이스를 명시적으로 처리하도록 강제한다. 이를 통해 외부 라이브러리 사용 시 발생할 수 있는 예기치 못한 부작용을 안전하게 래핑하여 관리하는 체계를 구축했다.

초기 테스트에서 LLM은 Brief의 엄격한 계약을 우회하려 시도했으나 시스템 프롬프트를 통해 논리 구조를 강제함으로써 성능을 개선했다. CLAUDE.md와 AGENTS.md 파일을 활용해 LLM 에이전트가 언어의 규칙을 준수하도록 유도했으며 그 결과 LLM이 스스로 코드를 검증하고 수정하는 워크플로우가 가능해졌다.

용어 해설

호어 트리플(Hoare Triple): — 프로그램의 로직이 올바른지 증명하기 위해 사용하는 세 가지 요소(전제 조건, 명령, 사후 조건)의 집합이다. Brief 언어에서는 함수 호출 전후의 상태를 엄격히 정의하여 컴파일 타임에 논리적 오류를 포착하는 핵심 메커니즘으로 활용된다.
선언형 프로그래밍(Declarative Programming): — 프로그램이 '어떻게(How)' 동작해야 하는지 명령을 나열하는 대신, '무엇(What)'이 진실인지 상태를 선언하는 방식이다. Brief는 이를 통해 프로그램 전체를 하나의 논리 엔진으로 변환하여 상태 간의 모순을 자동으로 찾아낸다.
외부 함수 인터페이스(FFI): — 한 프로그래밍 언어에서 다른 언어로 작성된 함수를 호출할 수 있게 해주는 메커니즘이다. Brief는 TOML 설정을 통해 외부 언어의 입출력을 자신의 논리 계약과 매핑하여 안전하지 않은 외부 세계와의 상호작용을 관리한다.
튜링 완전성(Turing Complete): — 어떤 계산 시스템이 튜링 머신과 동일한 계산 능력을 갖추고 있어, 이론적으로 모든 계산 가능한 문제를 풀 수 있음을 의미한다. Brief는 논리 기반 언어임에도 불구하고 범용 프로그래밍이 가능하도록 이 특성을 확보했다.

언급된 도구

Brief추천

논리 검증 기반의 선언형 프로그래밍 언어

Rust중립

Brief 컴파일러 구현 및 타겟 언어

언급된 리소스

GitHubBrief GitHub Repository