'완벽하게 구현해줘'라고 했더니 버튼 하나만 왔어요 — AI의 '완성'을 수학으로 정의하기

이 글에서 다룰 이야기

AI한테 "블로그 디자인해줘"라고 했어요. 결과물이 묘하게 괴상했어요. 보라색 그라데이션 배경에 둥근 카드가 줄지어 있고, 제목마다 이모지가 하나씩 붙어 있었어요. 딱히 틀린 데는 없는데, 누구의 취향도 아닌 화면이었어요. 혹시나 해서 "완벽하고 세련되게 해줘"를 붙여봤더니 그림자가 짙어지고 카드가 하나 늘었을 뿐이었어요.

그런데 agent.nexus 링크를 주면서 "이 사이트처럼 만들어줘"라고 하니 꽤 그럴듯한 결과가 나왔어요. 지금 보고 계신 이 블로그도 그렇게 만들었어요.

처음에는 AI의 실력 문제라고 생각했어요. 그런데 같은 AI도 요청을 어떻게 하느냐에 따라 결과가 크게 달라지더라고요. 이 글에서는 그 차이가 자연어의 모호함에서 온다고 보고, 자연어 요구사항을 형식 언어로 옮겨서 AI의 완료 조건으로 쓰는 방법을 정리했어요. 요구사항을 수식으로 적고, Bend라는 언어로 증명하고, fast-check로 실제 코드를 확인하는 과정이에요.

지난 글 마지막에 "기계가 보장하는 건 선언한 공간 안에서뿐"이라고 적었는데, 이번 글은 그 공간을 어떻게 정의하는지에 대한 이야기예요.

완벽한 구현은 "선언한 공간 전체에서, 적어둔 법칙을 지키는 구현"이에요. 공간과 법칙을 적지 않으면 '완벽'도 정의되지 않아요.

자연어로 시키면 왜 결과가 이상할까요

같은 AI인데 결과가 이렇게 갈리는 건 요청에 담긴 정보의 양이 달라서예요. 레퍼런스 사이트 하나에는 색, 글꼴, 간격, 레이아웃, 분위기가 전부 정해져 있어요. "세련되게"는 그중 어느 것도 정하지 않아요. 말한 사람 머릿속에는 분명한 그림이 있지만, 문장에는 그 그림이 들어 있지 않거든요.

자연어는 원래 듣는 사람이 빈칸을 채워줄 거라고 기대하는 언어예요. 사람끼리는 같이 일해온 경험이나 팀 분위기로 그 빈칸을 채워요. AI에게는 그런 맥락이 없어서, 정해지지 않은 부분을 가장 흔한 기본값으로 채워요. 결과가 괴상해 보이는 건 AI가 못해서라기보다, 빈칸이 너무 많은 요청을 받았기 때문이에요.

빈칸은 가장 짧은 길로 채워져요

코드도 마찬가지예요. AI는 요청을 끝내는 가장 짧은 길로 가요. 완료 조건이 "버튼이 있다"라면 버튼 하나를 만드는 게 가장 짧은 길이에요. "내보내기 버튼 만들어줘"라는 요청에 대한 가장 짧은 답은 대략 이런 모양이에요.

export function ExportButton() {
  return <button onClick={() => downloadCsv()}>내보내기</button>;
}

요청 문장만 보면 흠잡을 데가 없어요. 권한 검사나 화면 폭, 에러 처리는 요청에 없었으니까요. AI 입장에서 그런 일은 완료 조건에 없는 추가 비용이에요. 강화학습에서는 이런 현상을 specification gaming이라고 불러요. 보상 함수에 적힌 글자는 지키면서 설계자의 의도는 비껴가는 행동을 말해요.

"완벽하게"라는 말을 붙여도 빈칸은 그대로 남아요. 무엇이 완벽한지가 문장에 적혀 있지 않으니까요. AI가 가장 짧은 길로 가는 습관은 바꿀 수 없어요. 그래서 질문을 바꿔보기로 했어요. 그 짧은 길이 프로덕트 품질을 지나가게 하려면, 요청을 어떻게 적어야 할까요?

테스트까지 맡기면 구멍도 같이 생겨요

테스트까지 AI에게 맡기면 문제가 하나 더 생겨요. 같은 오해가 구현과 테스트에 똑같이 들어가거든요. 개발자가 AI에게 이렇게 보냈다고 해볼게요.

내보내기 버튼 붙여주세요. 편집자만 쓸 수 있게 해주시고, 모바일에서는 못 쓰게요. 테스트도 같이 부탁해요.

AI가 흔히 돌려주는 결과는 이래요.

export function canExport(ctx: ExportContext) {
  return ctx.authenticated && ctx.permission === "editor" && ctx.width > 768;
}

test("편집자는 내보낼 수 있다", () => {
  assert.equal(canExport({ authenticated: true, permission: "editor", width: 1440 }), true);
});
test("viewer는 내보낼 수 없다", () => {
  assert.equal(canExport({ authenticated: true, permission: "viewer", width: 1440 }), false);
});
test("모바일에서는 내보낼 수 없다", () => {
  assert.equal(canExport({ authenticated: true, permission: "editor", width: 375 }), false);
});

테스트 세 개가 모두 통과해요. 그런데 요청한 사람이 생각한 동작과는 세 군데가 달라요.

"편집자만"을 글자 그대로 === "editor"로 읽어서 admin이 버튼을 못 써요. 요청한 사람은 편집 권한이 있는 사람이라는 뜻으로 썼는데 말이에요.
"모바일"의 경계를 AI가 > 768로 정해서 폭이 딱 768인 태블릿 세로 화면이 막혀요. 테스트에는 375와 1440만 들어 있어서 768 근처는 아무도 확인하지 않았어요.
로그아웃 상태를 확인하는 테스트가 없어요. 나중에 누가 ctx.authenticated &&를 지워도 테스트는 계속 초록불이에요.

세 가지 모두 구현을 쓸 때 떠올린 장면이 그대로 테스트 입력이 되면서 생긴 일이에요. 구현이 놓친 상황은 테스트도 함께 놓치게 돼요.

결과가 맞는지 판정하는 기준을 오라클(oracle)이라고 해요. 자세한 내용은 test-oracle에 정리해뒀어요. 오라클까지 AI가 구현을 보고 만들면, 채점하는 사람이 학생 답안지를 보고 정답을 정하는 셈이에요. 첫 글에서 정답을 정할 수 있는 출처를 두 군데로 제한한 것도 이 때문이었어요. 그렇다면 정답은 어디에서 가져와야 할까요?

자연어를 형식 언어로 옮겨요

디자인에서는 레퍼런스 사이트가 빈칸을 한꺼번에 채워줘요. 기능 요구사항에서는 그 역할을 형식 언어에 맡겨볼 수 있을까요? 요청을 형식 언어로 바꿔 적기만 해서는 안 돼요. "내보내기 버튼 만들어줘"를 그대로 옮기면 "버튼이 있다"라는 법칙 하나가 나올 뿐이에요. 768을 포함할지, 거부 사유를 어떤 순서로 적을지 같은 빈칸은 번역한다고 채워지지 않고, 결국 사람이 정해야 해요.

형식 언어가 도와주는 건 그다음이에요. 형식 언어(formal language)는 문법과 뜻이 엄밀하게 정해져 있어서, 누가 읽어도 해석이 하나로 정해지는 언어예요. 수식이나 프로그래밍 언어가 그래요. width >= 768은 누가 읽어도 768을 포함하지만, "모바일에서는 못 쓰게"는 읽는 사람마다 경계가 달라요. 요구사항을 이런 언어로 적어두면 세 가지가 달라져요.

어디까지 다루는지 보여요. 요구사항이 어떤 상황들을 다루는지가 목록으로 드러나요. "모바일"이라고 넘어갔던 말이 320~3840 사이의 화면 폭이라는 축이 되고, 목록에 없는 상황은 빠져 있다는 게 눈에 보여요.
무엇을 지켜야 하는지 증명하기 쉬워져요. 규칙이 식으로 적혀 있으면, 모든 상황에서 규칙이 지켜지는지를 입력을 하나씩 넣어보지 않고 증명으로 확인할 수 있어요. 빠진 경우가 있으면 검사기가 그 자리를 짚어줘요.
무엇을 테스트해야 하는지 알 수 있어요. 증명이 경우를 나눈 지점이 테스트할 대표값이 되고, 규칙에 남은 비교식이 경계값이 돼요. 테스트 범위를 감으로 정하지 않아도 돼요.

빈칸을 채우는 건 여전히 사람이에요. 다만 형식 언어로 적으면 빈칸이 어디 있는지 보이고, 한 번 채운 결정은 증명과 테스트가 기계적으로 지켜줘요. 처음부터 축 목록에 넣지 않은 빈칸은 이걸로도 보이지 않는데, 이건 글 끝에서 다시 이야기할게요.

이 글에서는 세 단계로 옮겨요. 먼저 수식으로 공간과 법칙을 적고, Bend로 그 법칙이 맞는지 증명하고, fast-check로 실제 코드가 같은 답을 내는지 확인해요. 수식에 나오는 기호는 아래 네 가지가 전부예요. 수식마다 바로 아래에 풀어서 설명해뒀으니 그 부분만 읽으셔도 괜찮아요. 기호를 더 알고 싶으시면 형식 논리 기호 읽는 법을 참고해주세요.

기호	읽는 법
`∀x ∈ Ω`	공간 Ω에 속한 모든 x에 대해
`S ⊆ Ω`	S가 Ω 안에 다 들어감
`⇔`	양쪽이 같이 참이고 같이 거짓
`×`	두 집합에서 하나씩 고른 모든 조합

'완벽한 구현'을 수식 한 줄로 적어보면

막연한 "완벽"을 이렇게 쪼개볼게요.

Perfect(I) \iff \forall x \in \Omega,\quad P\big(x,\ \pi(I(x))\big)

구현 I가 완벽하다는 건, 공간 Ω에 있는 모든 입력 x에 대해 실행 결과를 π로 관찰했을 때 법칙 P가 성립한다는 뜻이에요. 시험에 비유하면 Ω는 시험 범위, P는 정답 기준, π는 채점할 때 보는 칸이에요. 시험 범위가 교과서 1쪽이면 학생은 1쪽만 공부하겠죠. 주어진 조건에서는 그게 가장 효율적이니까요. AI가 받는 요청도 똑같이 읽혀요.

"내보내기 버튼 만들어줘"를 세 칸에 나눠 담아보면 이래요.

	요청 문장 그대로	프로덕트 수준
`Ω` 어떤 상황들에서?	로그인한 admin이 넓은 화면에서 보는 1가지	로그인 2 × 역할 3 × 폭 3,521(320~3840) = 21,126가지
`P` 무엇이 지켜져야?	버튼이 있다	아래 규칙 4개
`π` 무엇을 보고 판단?	화면에 보이는지	켜짐 여부, 내보내기 횟수, 로그

요청 문장에는 없지만, 기획자가 당연하게 여긴 규칙은 이 네 가지예요.

로그인하지 않았으면 꺼져야 해요.
viewer는 꺼져야 해요.
폭이 768보다 좁으면 꺼져야 해요.
로그인한 editor나 admin이 폭 768 이상에서 보면 켜져야 해요.

마지막 4번을 빼먹기 쉬운데요. 1~3번만 있으면 버튼을 항상 꺼두는 구현도 규칙을 하나도 어기지 않아요. 운전을 안 하면 사고도 나지 않는 것처럼요. 하면 안 되는 것과 해야 하는 것을 둘 다 적어야 법칙이 완성돼요.

AI의 최단경로는 표의 왼쪽 열을 정확히 맞춰요. 프로덕트 품질로 올리려면 오른쪽 열을 채워서 완료 조건으로 넘겨야 해요. 채운 내용을 확인할 때는 두 도구를 써요. P가 논리적으로 맞는지는 Bend로 증명하고, 실제 코드가 그대로 동작하는지는 fast-check로 확인해요.

Bend: 법칙을 적고 증명을 써요

Bend는 Python처럼 들여쓰기로 쓰는 프로그래밍 언어예요. 이 글에서는 2.0.34 버전을 썼어요. 보통 언어처럼 함수를 만들 수 있고, 여기에 더해 "이 함수는 항상 이 성질을 지킨다"는 법칙과 그 증명까지 코드로 써서 검사기에 통과시킬 수 있어요.

누를 때마다 켜짐과 꺼짐이 뒤집히는 전등 스위치로 살펴볼게요.

import Base

# 함수
def toggle(b: Bool) -> Bool:
  match b:
    case True{}:
      False{}
    case False{}:
      True{}

# 법칙: 모든 b에 대해 두 번 뒤집으면 원래대로
law toggle_twice:
  for b: Bool
  {toggle(toggle(b)) == b : Bool}

# 증명: 법칙과 이름이 같은 def
def toggle_twice(b):
  match b:
    case True{}:
      {==}
    case False{}:
      {==}

match는 값에 따라 경우를 나눠요. 가능한 경우를 하나라도 빼먹으면 검사를 통과하지 못해요.
for b: Bool은 "모든 Bool 값 b에 대해"라는 뜻이에요. 수식의 ∀b와 같아요.
{==}는 "양쪽을 계산해보면 똑같다"는 뜻이에요. b가 True{}라면 toggle(toggle(True{}))는 toggle(False{})를 거쳐 True{}가 돼요.

Bool은 값이 두 개뿐이라, 두 경우를 다 보여주면 "모든 b"에 대한 증명이 끝나요.

$ bend toggle.bend
ALL PROOFS CHECK

toggle이 True{}를 받아도 True{}를 돌려주도록 일부러 망가뜨려 봤어요. 검사기가 어느 경우에서 깨졌는지 줄 번호까지 짚어서 거절해요.

SOME PROOFS FAIL
Error:
- expected : True{}
- observed : False{}
Location: toggle_twice
18 |     case False{}:
19>|       {==}

TypeScript였다면 무조건 true만 돌려주는 toggle도 타입 검사를 통과했을 거예요. boolean을 받아서 boolean을 돌려주니까요. TypeScript의 타입 검사는 어떤 종류의 값이 오가는지까지만 보고, Bend는 법칙이 있어서 맞는 값이 오가는지까지 봐요.

실제 프로젝트에서는 법칙을 LAWS.bend에, 증명을 PROOF.bend에 나눠 담아요. 사람은 무엇이 참이어야 하는지만 LAWS.bend에 적고, AI는 코드와 증명을 함께 써와요. 증명이 통과하지 않으면 완성으로 치지 않아요. --verdict 옵션을 붙이면 Lean으로 증명된 작은 커널이 결과를 한 번 더 확인해줘요.

fast-check: 성질을 적으면 입력은 알아서 만들어요

Bend가 증명하는 대상은 Bend로 쓴 모델이에요. 실제 앱은 TypeScript로 돌아가니까, 실제 코드는 테스트로 확인해야 해요.

fast-check는 JavaScript와 TypeScript에서 쓰는 속성 기반 테스트(property-based testing) 라이브러리예요. 보통 테스트처럼 예시를 하나씩 적는 대신 성질을 적어요. 볼륨을 0~100으로 제한하는 함수를 만들다가 음수 처리를 빠뜨렸다고 해볼게요.

const clamp = (n: number) => Math.min(Math.max(n, 0), 100);
const buggyVolume = (n: number) => (n > 50 ? clamp(n) : n); // 음수 처리 누락

fc.assert(
  fc.property(fc.integer(), (n) => {
    const v = buggyVolume(n);
    return v >= 0 && v <= 100;
  }),
);

Property failed after 2 tests
Counterexample: [-1]
Shrunk 31 time(s)

fc.integer()는 정수 입력을 만들어주는 생성기예요. fast-check에서는 arbitrary라고 불러요.
fc.property(생성기, 검사 함수)는 "생성기가 만든 어떤 값을 넣어도 검사 함수가 참이다"라는 성질이에요. Bend의 law와 같은 모양의 주장을 TypeScript로 적은 거예요.
fc.assert는 기본으로 입력을 100개 만들어 넣어봐요. 실패하면 실패가 유지되는 범위에서 입력을 계속 줄여서(shrinking) 가장 단순한 반례인 -1을 보여줘요.

실제 코드를 직접 돌려본다는 게 fast-check의 장점이고, 넣어본 입력까지만 보장한다는 게 한계예요. 두 도구가 보장하는 범위를 나란히 적으면 이래요.

\forall x \in \Omega,\ P(x, M(x)) \qquad \forall x \in S,\ P(x, I(x)),\ \ S \subseteq \Omega

왼쪽은 Bend가 모델 M에 대해 모든 입력에서 주는 보장이고, 오른쪽은 fast-check가 구현 I에 대해 넣어본 입력 S에서 주는 보장이에요. 증명은 모델까지만 가고, 구현까지는 테스트로 이어줘야 해요. 그래서 S를 잘 고르는 게 중요한데, 고르는 방법이 증명된 모델 안에 이미 들어 있어요. 3단계에서 보여드릴게요.

1단계: 버튼의 켜짐/꺼짐을 Bend로 풀어요

이제 내보내기 버튼으로 돌아올게요. 요구사항을 한 문장으로 적으면 이래요.

로그인한 editor 또는 admin은 화면 폭이 768 CSS 픽셀 이상일 때 내보내기 버튼을 쓸 수 있다.

폭은 정수로, 768은 포함으로, 편집 권한은 {editor, admin}으로 정했어요. 모델에 나오는 Nat.is_ge(width, 768n)은 width >= 768과 같은 뜻이에요.

# export.bend
import Base

type Role is Data:
  Viewer{}
  Editor{}
  Admin{}

def can_edit(r: Role) -> Bool:
  match r:
    case Viewer{}:
      False{}
    case Editor{}:
      True{}
    case Admin{}:
      True{}

def enabled(auth: Bool, r: Role, width: Nat) -> Bool:
  match auth:
    case False{}:
      False{}
    case True{}:
      can_edit(r) && Nat.is_ge(width, 768n)

법칙은 두 개를 적었어요. 하나는 "로그인하지 않았으면 역할과 폭에 상관없이 꺼진다", 다른 하나는 "폭이 768 이상인 editor는 켜진다"예요. 두 번째 법칙이 없으면 항상 꺼져 있는 모델도 첫 번째 법칙을 통과해요. 앞에서 본 운전을 안 해서 생긴 무사고 기록과 같은 경우인데, 논리학에서는 공허한 참(vacuous truth)이라고 불러요.

# LAWS.bend
import Base
import ./export.bend as E

law guest_is_disabled:
  for r: E.Role
  for width: Nat
  {E.enabled(False{}, r, width) == False{} : Bool}

law wide_editor_is_enabled:
  for width: Nat
  for wide: {Nat.is_ge(width, 768n) == True{} : Bool}
  {E.enabled(True{}, E.Editor{}, width) == True{} : Bool}

# PROOF.bend
import Base
import ./LAWS.bend as Laws

def Laws.guest_is_disabled(r, width):
  {==}

def Laws.wide_editor_is_enabled(width, wide):
  wide

$ bend PROOF.bend --verdict
ALL PROOFS CHECK

로그인하지 않았으면 enabled가 첫 번째 case에서 바로 False{}가 되기 때문에, {==} 하나로 모든 폭과 역할에 대해 한 번에 증명이 끝나요. 두 번째 법칙은 계산하고 나면 목표가 가정 wide와 똑같은 모양이 돼서, wide를 그대로 돌려주면 돼요.

모델의 >= 768을 > 768로 바꿔보면 검사기가 거절해요.

SOME PROOFS FAIL
Error:
- expected : {Cmp.is_gt(Nat.cmp(width, 768n)) == True{} : Bool}
- observed : {Cmp.is_ge(Nat.cmp(width, 768n)) == True{} : Bool}

입력을 하나도 넣어보지 않고, 768에서 법칙이 깨진다는 걸 알아낸 거예요.

2단계: 로그 요구사항이 붙으면

기획서에 한 줄이 추가됐다고 해볼게요.

내보내기 버튼을 누르면 로그를 남겨주세요.

AI의 최단경로는 이래요.

export function handleExportClick(ctx: ExportContext, { exportCsv, log }: Deps) {
  const enabled = ctx.authenticated && ctx.permission !== "viewer" && ctx.width > 768;
  if (!enabled) return;
  exportCsv();
  log({ kind: "exported", role: ctx.permission });
}

요청 문장은 만족해요. 눌러서 내보내지면 로그가 남으니까요. 그런데 꺼진 버튼을 눌렀을 때는 아무 기록도 남지 않아서, "왜 내보내기가 안 되죠?"라는 문의에 로그로 답할 수가 없어요. 768 버그도 그대로 남아 있고요.

버튼 하나일 때는 결과가 true/false 두 가지였는데, 로그가 붙으면 결과가 "무엇이 기록됐나"로 늘어나요. Bend에서는 이걸 타입으로 먼저 적어요.

type Reason is Data:
  Guest{}
  NoPermission{}
  TooNarrow{}

type Log is Data:
  Exported{role: Role}
  Denied{reason: Reason}

타입을 적는 순간 정책 질문이 튀어나와요. 꺼진 버튼을 누르면 무엇을 남겨야 할까요? 로그인도 안 했고 폭도 좁으면 사유는 뭐라고 적어야 할까요? 저는 "누를 때마다 로그는 정확히 하나, 사유는 로그인 → 권한 → 폭 순서로 먼저 걸린 것"으로 정했어요. 이 순서는 수학으로 정해지지 않아서 사람이 정책으로 정해야 해요.

정한 대로 클릭을 모델링하면 이렇게 돼요.

def check_width(r: Role, wide: Bool) -> Log:
  match wide:
    case True{}:
      Exported{r}
    case False{}:
      Denied{TooNarrow{}}

def check_role(r: Role, width: Nat) -> Log:
  match r:
    case Viewer{}:
      Denied{NoPermission{}}
    case Editor{}:
      check_width(Editor{}, Nat.is_ge(width, 768n))
    case Admin{}:
      check_width(Admin{}, Nat.is_ge(width, 768n))

def click(auth: Bool, r: Role, width: Nat) -> Log:
  match auth:
    case False{}:
      Denied{Guest{}}
    case True{}:
      check_role(r, width)

def is_exported(l: Log) -> Bool:
  match l:
    case Exported{_}:
      True{}
    case Denied{_}:
      False{}

법칙도 두 개 추가했어요.

law log_matches_button:
  for auth: Bool
  for r: E.Role
  for width: Nat
  {E.is_exported(E.click(auth, r, width)) == E.enabled(auth, r, width) : Bool}

law guest_reason:
  for r: E.Role
  for width: Nat
  {E.click(False{}, r, width) == E.Denied{E.Guest{}} : E.Log}

log_matches_button은 "로그와 버튼이 절대 엇갈리지 않는다"는 법칙이에요. Exported 로그는 버튼이 켜지는 입력에서만 남고, 그런 입력에서는 반드시 남아요. guest_reason은 "로그인하지 않았으면 역할과 폭이 무엇이든 사유는 Guest"라는 법칙이고요. 앞에서 정한 사유 순서를 법칙으로 못 박은 거예요.

\forall a, r, w,\quad isExported(click(a, r, w)) \iff enabled(a, r, w)

증명은 경우를 나눠서 써요.

def export_agrees(r: E.Role, wide: Bool) -> {E.is_exported(E.check_width(r, wide)) == wide : Bool}:
  match wide:
    case True{}:
      {==}
    case False{}:
      {==}

def Laws.log_matches_button(auth, r, width):
  match auth r:
    case False{} _:
      {==}
    case True{} E.Viewer{}:
      {==}
    case True{} E.Editor{}:
      export_agrees(E.Editor{}, Nat.is_ge(width, 768n))
    case True{} E.Admin{}:
      export_agrees(E.Admin{}, Nat.is_ge(width, 768n))

def Laws.guest_reason(r, width):
  {==}

$ bend PROOF.bend --verdict
ALL PROOFS CHECK

match auth r에 나오는 네 경우를 보세요. 비로그인, viewer, editor, admin이에요. 증명이 경우를 나눈 선이 그대로 입력 공간을 나누는 선이 돼요. 테스트 설계에서 동등 분할(equivalence partitioning)이라고 부르는 작업을 증명이 먼저 해준 셈이에요. 그리고 editor와 admin 경우에 끝까지 남는 Nat.is_ge(width, 768n)이 바로 경계값이에요.

3단계: 증명된 모델을 fast-check로 투영해요

이제 남은 건 실제 TypeScript가 이 모델대로 동작하는지 확인하는 일이에요. Bend 모델은 JavaScript 모듈로 빌드할 수 있어서, fast-check의 정답지로 바로 불러올 수 있어요.

bend export.bend -o export-model.mjs

테스트에 필요한 세 가지는 모두 모델에서 가져와요.

관찰 함수 π는 법칙에 나오는 것으로 정해요. 법칙이 말하는 건 내보내기 여부와 로그라서, 실행 결과에서 내보내기 횟수와 로그 목록만 떼어서 비교해요. π에 켜짐 여부만 넣었다면 로그 버그는 하나도 보이지 않았을 거예요.
동등 분할은 증명의 네 경우에서 가져와요. 경우마다 대표값을 하나씩 고르고, 나머지 축은 일부러 헷갈리게 골라요. 예를 들어 비로그인 대표값을 admin에 좁은 폭으로 잡으면, 사유 순서를 뒤집은 구현은 Guest 대신 TooNarrow를 남겨서 걸려요.
경계값은 모델의 Nat.is_ge(width, 768n)에서 767, 768, 769를 뽑아요. 이건 무작위에 맡기면 안 돼요. 21,126가지 입력 중 768 버그가 드러나는 입력은 2개뿐이라서, 경계 예제 없이 무작위로 1,000번을 돌렸더니 100번 중 89번은 버그를 놓쳤어요.

나머지 공간은 무작위 1,000회로 훑어요. Node 26의 기본 테스트 러너와 fast-check 4.10.2로 돌렸고, 타입 import는 생략했어요.

import { test } from "node:test";
import assert from "node:assert/strict";
import fc from "fast-check";
import Model from "./export-model.mjs";
import { handleExportClick } from "./export-button";

// π: 실행 결과 중 법칙이 보는 것만 골라요
function observe(ctx: ExportContext) {
  let exports = 0;
  const logs: LogEntry[] = [];
  handleExportClick(ctx, { exportCsv: () => exports++, log: (e) => logs.push(e) });
  return { exports, logs };
}

// 증명된 Bend 모델의 결과를 같은 모양으로 옮겨요
const reasons = { Guest: "guest", NoPermission: "no-permission", TooNarrow: "too-narrow" };
function expected(ctx: ExportContext) {
  const role = { $: ctx.permission[0].toUpperCase() + ctx.permission.slice(1) };
  const log = Model.click(ctx.authenticated, role, BigInt(ctx.width));
  return log.$ === "Exported"
    ? { exports: 1, logs: [{ kind: "exported", role: ctx.permission }] }
    : { exports: 0, logs: [{ kind: "denied", reason: reasons[log.reason.$] }] };
}

// 동등 분할: 증명의 네 경우마다 대표값 하나. 다른 축은 헷갈리게 골라요
const partitions: ExportContext[] = [
  { width: 500, authenticated: false, permission: "admin" }, // Guest
  { width: 1440, authenticated: true, permission: "viewer" }, // NoPermission
  { width: 500, authenticated: true, permission: "editor" }, // TooNarrow
  { width: 1440, authenticated: true, permission: "admin" }, // Exported
];

// 경계값: 모델의 is_ge(width, 768n)에서
const boundaries: ExportContext[] = [767, 768, 769].map((width) => ({
  width,
  authenticated: true,
  permission: "editor",
}));

const contextArbitrary = fc.record({
  width: fc.integer({ min: 320, max: 3840 }),
  authenticated: fc.boolean(),
  permission: fc.constantFrom<Permission>("viewer", "editor", "admin"),
});

test("클릭 결과가 증명된 모델과 같다", () => {
  fc.assert(
    fc.property(contextArbitrary, (ctx) => {
      assert.deepEqual(observe(ctx), expected(ctx));
    }),
    {
      seed: 20260930,
      numRuns: 1000,
      examples: [...partitions, ...boundaries].map((ctx) => [ctx]),
    },
  );
});

examples에 넣은 값은 무작위 값보다 먼저 실행돼요. 그래서 분할 대표값 4개와 경계값 3개가 항상 맨 앞에서 검사돼요. 구현을 바꿔가며 돌려본 결과는 이랬어요.

구현	결과
AI의 최단경로 (성공할 때만 로그, `> 768`)	1번째 입력에서 실패. 비로그인 클릭에 로그가 없음
거부 로그 추가, `> 768`은 그대로	6번째 입력(768)에서 실패
사유 순서를 폭 → 로그인으로 뒤집음	1번째 입력에서 실패. `Guest` 대신 `TooNarrow`
거부 로그 + `>= 768`	1,000회 통과

AI에게 넘기는 완료 조건도 이렇게 바꿔요.

완료 조건
1. bend PROOF.bend --verdict 가 ALL PROOFS CHECK  (LAWS.bend는 수정 금지)
2. fast-check 테스트 통과                         (분할 대표값 + 경계값 + 무작위 1,000회)
3. 정하지 못한 정책은 NEEDS_DECISION으로 보고

"완벽하게 해줘"보다 훨씬 좁은 조건이에요. 그런데 AI가 이 조건을 가장 짧은 길로 통과하려고 해도, 거부 로그와 사유 순서와 768을 전부 거쳐야 해요.

정직하게: 이걸로도 못 잡는 것

증명은 모델까지, 테스트는 넣어본 입력까지만 보장해요. 그래서 정의 자체가 틀리면 둘 다 통과해요. 경계를 1000으로 잘못 적어도 증명은 성립하고, 테스트는 그 틀린 모델을 충실히 따라가요.
모델과 실제 코드를 잇는 연결 코드도 틀릴 수 있어요. 저는 처음에 Bend의 Bool을 { $: "False" } 객체로 넘기는 바람에, 모델이 비로그인을 True로 읽었어요. 빨간불이 났다고 해서 구현이 틀린 건 아니었던 거죠.
같은 AI가 모델과 구현을 둘 다 쓰면 같은 오해가 양쪽에 들어갈 수 있어요. 증명이 안 될 때 법칙을 약하게 고치는 게 AI에게는 가장 짧은 길이라서, LAWS.bend만큼은 사람이 쓰고 첫 글처럼 해시로 잠가두는 게 좋아요.
선언한 공간 밖은 볼 수 없어요. 이 한계는 정리에서 조금 더 이야기해볼게요.

정리

"완벽하게 구현해줘"를 붙여도 결과가 거의 같았던 건, 완료 조건이 여전히 "버튼이 있다" 하나였기 때문이에요. 그래서 AI에게 일을 넘기기 전에 제가 먼저 하는 일을 바꿨어요.

요구사항이 어떤 축으로 이루어져 있는지 적어요. "내보내기 버튼" 한 줄에도 로그인 여부, 권한, 화면 폭이라는 축이 숨어 있었어요. 이 축들이 공간 Ω가 되고, 각 상황에서 지켜야 할 규칙은 P, 무엇을 보고 판단할지는 π가 돼요.
그 이해를 증명으로 확인해요. "다 생각한 것 같다"는 감으로 넘어가는 대신 Bend 모델에 대해 P를 증명해요. 증명은 같은 모델에 늘 같은 판정을 내리고, 누가 어떻게 해석하느냐에 따라 달라지지 않아요. 증명하면서 경우를 나눈 지점은 동등 분할이 되고, 끝까지 남는 비교식은 경계값이 돼요.
증명된 모델을 테스트의 정답지로 써요. 실제 코드에 분할 대표값, 경계값, 무작위 입력을 넣고, 모델과 같은 답을 내는지 확인해요.

이렇게 했더니 "로그 남겨주세요" 한 줄에 숨어 있던 거부 로그, 사유의 우선순위, 768 경계가 첫 몇 개 입력 안에서 모두 걸렸어요. AI는 지금도 가장 짧은 길로 가요. 다만 이제는 그 길이 "선언한 공간 전체에서 적어둔 법칙을 지킨다"에 도착해야 끝나요.

남은 문제: 공간은 누가 정하나요

증명은 선언한 Ω 안에서 P를 어기는 입력이 없다는 것까지 보여줘요. 하지만 Ω 밖은 보지 못해요. "내보내는 중에 또 누르면?"이 그런 경우였어요. 처음 정한 공간에는 진행 상태라는 시간 축이 없었기 때문에, 증명도 테스트도 이 질문을 던지지 않았어요. 이런 건 제보나 탐색 테스트로 발견한 뒤에 Ω₁ = Ω × {idle, exporting}처럼 축을 늘리고 법칙을 다시 적어야 해요.

공간 안에서 법칙이 성립한다는 건 증명할 수 있어요. 그런데 그 공간이 내가 원한 상황을 충분히 담고 있는지는 형식적으로 증명할 수 없어요. 비교할 기준이 사람의 의도이기 때문이에요. 브라이언 캔트웰 스미스도 1985년에 같은 한계를 지적했어요. 소프트웨어 공학에서는 앞의 것을 검증(verification), 뒤의 것을 확인(validation)이라고 나눠 불러요.

그래서 사람에게 남는 어려운 일은 증명보다 앞 단계에 있어요. 문제를 어떤 축으로 쪼갤지, 그 축을 AI가 같은 뜻으로 이해하게 하려면 어떻게 전달할지, "로그 남겨주세요" 같은 모호한 자연어를 내 의도대로 축과 법칙으로 풀어낼 수 있을지요. 코드를 쓰는 일은 점점 AI가 맡고, 맞게 썼는지 확인하는 일은 증명과 테스트가 맡게 될 거예요. 그러면 개발자의 일은 "무엇이 맞는 것인가"를 정하는 쪽으로 옮겨가지 않을까 싶어요.

다음에 AI에게 기능을 맡길 때는 "완벽하게" 대신 세 가지를 먼저 적어보세요. 어떤 상황들이 있는지, 각 상황에서 무엇이 지켜져야 하는지, 그리고 무엇을 보고 확인할지요.

참고 자료

본문에서 기댄 도구 동작과 주장의 출처예요. 예제 계약, 로그 정책, 완료 조건 형식은 이 글에서 제안하는 설계예요.

Bend

bendlang/bend — README — law/proof 구조, proof search 없음, --verdict 커널
bendlang/bend — GUIDE.md — LAWS.bend/PROOF.bend 관례, match와 증명 작성법, -o .mjs로 JavaScript에서 부르는 방법

fast-check

What is Property-Based Testing? — 입력 생성, seed, shrinking 개념
User definable values — examples가 무작위 값보다 먼저 실행된다는 설명

테스트 설계

ASTQB — 4.2 Black-Box Test Techniques — 동등 분할과 경계값 분석

검증의 한계와 요구사항

Brian Cantwell Smith (1985), The Limits of Correctness — 증명은 프로그램과 모델 사이의 관계까지만 보여주고, 모델과 현실 사이는 다루지 못한다는 논증
Barry Boehm (1984), Verifying and Validating Software Requirements and Design Specifications — 검증(제대로 만들었나)과 확인(맞는 걸 만들었나)의 구분
Pamela Zave, Michael Jackson (1997), Four Dark Corners of Requirements Engineering — 요구사항은 바깥 세계에 대한 문장이고, 명세는 세계에 대한 가정과 함께 요구사항을 만족한다는 틀
Edsger W. Dijkstra (1970), Notes on Structured Programming (EWD249) — 테스트는 버그가 있음을 보여줄 수는 있어도 없음을 보여주지는 못한다는 지적
Bowen Alpern, Fred B. Schneider (1985), Defining Liveness — 성질을 실행 순서 전체에 대한 조건으로 보고 safety와 liveness로 나누는 정의
Cosler et al. (2023), nl2spec: Interactively Translating Unstructured Natural Language to Temporal Logics with Large Language Models — LLM으로 자연어 요구사항을 시제 논리로 옮기고, 모호한 부분을 사람과 상호작용하며 고치는 연구