I Asked for a Perfect Implementation and Got One Button — Defining AI's 'Done' Mathematically

What this post covers

I asked AI to "design my blog." What came back was oddly off. A purple gradient background, rows of rounded cards, an emoji on every heading. Nothing was exactly wrong, but it was a screen that matched nobody's taste. Just in case, I added "make it perfect and polished." All that changed was darker shadows and one more card.

Then I gave it a link to agent.nexus and said "make it like this site," and the result was quite convincing. The blog you are reading now was built that way.

At first I thought it was a matter of AI's skill. But the same AI gave very different results depending on how I asked. This post traces that gap to the ambiguity of natural language, and walks through a way to translate natural-language requirements into a formal language and use them as AI's completion condition: writing requirements as formulas, proving them in a language called Bend, and checking the real code with fast-check.

At the end of the last post, I wrote that "machines only guarantee what holds inside the declared space." This post is about how to define that space.

A perfect implementation is "one that keeps the written laws across the whole declared space." If you do not write down the space and the laws, "perfect" is not defined either.

Why do natural-language requests give strange results?

The same AI splits this way because the two requests carry different amounts of information. A single reference site pins down color, typefaces, spacing, layout, and mood. "Polished" pins down none of them. The person asking has a clear picture in mind, but the sentence does not contain that picture.

Natural language expects the listener to fill in the blanks. Between people, shared work history and team culture fill them. AI has no such context, so it fills whatever is left undecided with the most common defaults. The result looks strange less because AI is bad at the job and more because it received a request with too many blanks.

Blanks get filled by the shortest path

Code works the same way. AI takes the shortest path to finishing the request. If the completion condition is "a button exists," building one button is the shortest path. The shortest answer to "build an export button" looks roughly like this.

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

Read against the request alone, there is nothing to fault. Permission checks, screen width, and error handling were not in the request. From AI's side, that work is extra cost outside the completion condition. Reinforcement learning calls this specification gaming: behavior that keeps the letter of the reward function while missing the designer's intent.

Adding "perfectly" leaves the blanks as they are, because the sentence still does not say what perfect means. AI's habit of taking the shortest path cannot be changed. So I changed the question instead. How should the request be written so that the shortest path runs through product quality?

Assigning the tests creates the holes too

Hand the tests to AI as well, and another problem appears: the same misunderstanding goes into both the implementation and the tests. Say a developer sends AI this:

Please add an export button. Only editors should be able to use it, and it shouldn't work on mobile. Tests too, please.

What AI commonly returns looks like this.

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

test("editors can export", () => {
  assert.equal(canExport({ authenticated: true, permission: "editor", width: 1440 }), true);
});
test("viewers cannot export", () => {
  assert.equal(canExport({ authenticated: true, permission: "viewer", width: 1440 }), false);
});
test("cannot export on mobile", () => {
  assert.equal(canExport({ authenticated: true, permission: "editor", width: 375 }), false);
});

All three tests pass. Yet the behavior differs from what the requester had in mind in three places.

• AI read "only editors" literally as === "editor", so admins cannot use the button. The requester meant people with edit permission.
• AI chose > 768 as the "mobile" boundary, so a portrait tablet at exactly 768 is blocked. The tests only contain 375 and 1440, so nobody checked anything near 768.
• There is no test for the logged-out state. If someone later deletes ctx.authenticated &&, the tests stay green.

All three happened because the scenes imagined while writing the implementation became the test inputs. Whatever the implementation misses, the tests miss with it.

The standard used to judge whether a result is correct is called an oracle. I explain it in more detail in test-oracle. If AI builds the oracle by looking at the implementation, it is like a grader deciding the correct answer by reading the student's answer sheet. That is also why the first post limited the sources allowed to define the answer to two. So where should the answer come from?

Translating natural language into a formal language

In design, a reference site fills the blanks all at once. Can a formal language play that role for functional requirements? Simply rewriting the request in a formal language is not enough. Translate "build an export button" as is, and all you get is a single law, "a button exists." Blanks such as whether 768 is included, or in what order to record denial reasons, are not filled by translation. In the end, a person has to decide them.

What a formal language helps with comes after that. A formal language has strictly defined grammar and meaning, so anyone who reads it arrives at the same single interpretation. Mathematical formulas and programming languages are like this. Anyone reading width >= 768 knows it includes 768, while "it shouldn't work on mobile" puts the boundary somewhere different for each reader. Writing requirements in such a language changes three things.

• You can see how far the requirement reaches. Which situations the requirement covers shows up as a list. What was glossed over as "mobile" becomes an axis of screen widths from 320 to 3840, and any situation missing from the list is visibly missing.
• What must hold becomes easier to prove. When rules are written as expressions, you can confirm that they hold in every situation with a proof instead of trying inputs one by one. If a case is missing, the checker points to the spot.
• You know what needs testing. The points where the proof splits cases become the representative values to test, and the comparison left in a rule becomes the boundary value. You no longer have to set the test scope by feel.

Filling the blanks is still a person's job. But once requirements are written in a formal language, you can see where the blanks are, and proofs and tests mechanically keep each decision once it is made. Blanks that never made it onto the axis list stay invisible even then, and I come back to that at the end of the post.

This post translates in three steps. First, write the space and laws as formulas. Then prove the laws in Bend, and finally check with fast-check that the real code gives the same answers. The formulas use only the four symbols below. Each formula is explained in plain words right below it, so reading only those parts is fine. For more on the symbols, see how to read formal logic notation.

Writing "perfect implementation" as one formula

Let's break the vague word "perfect" down like this.

An implementation I is perfect when, for every input x in the space Ω, the law P holds once the result is observed through π. As an exam, Ω is the exam scope, P is the answer key, and π is the boxes the grader looks at. If the scope is page 1 of the textbook, a student studies only page 1. Under the given conditions, that is the most efficient choice. AI reads requests the same way.

Here is "build an export button" split into the three slots.

The request does not mention them, but these are the four rules the planner took for granted.

1. If not logged in, it must be disabled.
2. A viewer must see it disabled.
3. If the width is narrower than 768, it must be disabled.
4. A logged-in editor or admin at width 768 or more must see it enabled.

Rule 4 is easy to forget. With only rules 1 to 3, an implementation that always keeps the button disabled breaks none of them, the same way you never have an accident if you never drive. A law is complete only when it states both what must not happen and what must.

AI's shortest path matches the left column of the table exactly. Raising it to product quality means filling in the right column and handing it over as the completion condition. To check what we filled in, we use two tools: Bend proves that P is logically right, and fast-check confirms that the real code behaves the same way.

Bend: write a law, then write its proof

Bend is a programming language indented like Python. This post uses version 2.0.34. You can write functions as in any language, and on top of that you can write a law, "this function always keeps this property," and its proof as code and pass them through a checker.

Let's look at a light switch that flips between on and off each time you press it.

import Base

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

# law: for every b, flipping twice gives back the original
law toggle_twice:
  for b: Bool
  {toggle(toggle(b)) == b : Bool}

# proof: a def with the same name as the law
def toggle_twice(b):
  match b:
    case True{}:
      {==}
    case False{}:
      {==}

• match splits into cases by value. If you leave out even one possible case, it fails the check.
• for b: Bool means "for every Bool value b." It is the same as ∀b in a formula.
• {==} means "compute both sides and they are the same." If b is True{}, toggle(toggle(True{})) goes through toggle(False{}) and becomes True{}.

Bool has only two values, so showing both cases completes the proof for "every b."

$ bend toggle.bend
ALL PROOFS CHECK

I deliberately broke toggle so that it returns True{} even when given True{}. The checker rejects it and points to the case that broke, down to the line number.

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

In TypeScript, a toggle that always returns true would pass the type check, since it takes a boolean and returns a boolean. TypeScript's type check looks only at what kind of value passes through. Bend has laws, so it also checks whether the right value passes through.

In a real project, laws go in LAWS.bend and proofs in PROOF.bend. A person writes only what must be true in LAWS.bend, and AI brings back the code together with the proofs. If the proofs do not pass, the work does not count as done. Adding the --verdict option has a small kernel, itself proved in Lean, check the result once more.

fast-check: write a property and it creates the inputs

What Bend proves is the model written in Bend. The real app runs on TypeScript, so the real code has to be checked with tests.

fast-check is a property-based testing library for JavaScript and TypeScript. Instead of writing examples one by one as in ordinary tests, you write a property. Say you build a function that limits volume to 0 to 100 and forget to handle negative numbers.

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() is a generator that creates integer inputs. fast-check calls it an arbitrary.
• fc.property(generator, check) is the property "whatever value the generator creates, the check is true." It is the same shape of claim as Bend's law, written in TypeScript.
• fc.assert creates and tries 100 inputs by default. When it fails, it keeps shrinking the input while the failure still holds, and shows the simplest counterexample, -1.

fast-check's strength is that it runs the real code, and its limit is that it guarantees only the inputs it tried. Side by side, the guarantees of the two tools look like this.

The left side is the guarantee Bend gives for the model M over every input, and the right side is the guarantee fast-check gives for the implementation I over the tried inputs S. The proof reaches only the model, so tests have to carry it to the implementation. That makes choosing S well important, and the way to choose it is already inside the proved model. Step 3 shows how.

Step 1: solve the button's enabled/disabled state in Bend

Back to the export button. Written as one sentence, the requirement is this.

A logged-in editor or admin can use the export button when the screen width is 768 CSS pixels or more.

I decided that width is an integer, 768 is included, and edit permission means {editor, admin}. The Nat.is_ge(width, 768n) in the model means the same as 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)

I wrote two laws. One is "if not logged in, it is disabled regardless of role and width," and the other is "an editor at width 768 or more sees it enabled." Without the second law, a model that is always disabled also passes the first. It is the same no-accident record from never driving, and logic calls it 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

If the user is not logged in, enabled becomes False{} right at the first case, so a single {==} proves it for every width and role at once. For the second law, once computed, the goal takes exactly the shape of the assumption wide, so returning wide as is completes it.

Change the model's >= 768 to > 768 and the checker rejects it.

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

Without trying a single input, it found that the law breaks at 768.

Step 2: when a logging requirement is added

Say one line is added to the spec.

Please leave a log when the export button is clicked.

AI's shortest path is this.

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 });
}

It satisfies the request: clicking and exporting leaves a log. But clicking a disabled button records nothing, so logs cannot answer the support question "why can't I export?" The 768 bug is still there, too.

With just a button, the result was true or false. Once logs are added, the result grows into "what was recorded." In Bend, we write that as a type first.

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

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

The moment you write the type, policy questions pop up. What should a click on a disabled button record? If the user is logged out and the screen is narrow, which reason should it give? I decided "exactly one log per click, and the reason is the first one hit in the order login → permission → width." Mathematics does not decide this order, so a person has to decide it as policy.

Modeling the click as decided gives this.

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{}

I added two laws as well.

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 is the law "the log and the button never disagree." An Exported log is left only for inputs where the button is enabled, and is always left for such inputs. guest_reason is the law "if not logged in, the reason is Guest whatever the role and width," which pins down the reason order decided above.

The proof is written by splitting cases.

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

Look at the four cases in match auth r: logged out, viewer, editor, and admin. The lines along which the proof split cases become the lines that split the input space. The proof has already done what test design calls equivalence partitioning. And Nat.is_ge(width, 768n), which remains to the end in the editor and admin cases, is exactly the boundary value.

Step 3: project the proved model into fast-check

What remains is checking that the real TypeScript behaves like this model. A Bend model can be built into a JavaScript module, so fast-check can load it directly as the oracle.

bend export.bend -o export-model.mjs

All three things the test needs come from the model.

• The observation function π is chosen from what the laws mention. The laws talk about whether an export happened and about logs, so we take only the export count and the log list from the run and compare those. If π had held only the enabled state, none of the log bugs would have shown.
• The equivalence partitions come from the proof's four cases. We pick one representative per case and deliberately choose the other axes to be confusing. For example, if the logged-out representative is an admin on a narrow screen, an implementation that reverses the reason order leaves TooNarrow instead of Guest and gets caught.
• The boundary values 767, 768, and 769 come from the model's Nat.is_ge(width, 768n). These must not be left to randomness. Only 2 of the 21,126 inputs expose the 768 bug, so running 1,000 random inputs without boundary examples missed the bug in 89 out of 100 runs.

The rest of the space is swept with 1,000 random runs. I ran it with Node 26's built-in test runner and fast-check 4.10.2, and omitted the type imports.

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]),
    },
  );
});

Values in examples run before the random values, so the 4 partition representatives and 3 boundary values are always checked first. Here is what happened when I swapped implementations.

The completion condition handed to AI changes accordingly.

Completion conditions
1. bend PROOF.bend --verdict prints ALL PROOFS CHECK (LAWS.bend is read-only)
2. fast-check tests pass (partition representatives + boundary values + 1,000 random runs)
3. Report any undecided policy as NEEDS_DECISION

This is a much narrower condition than "make it perfect." Yet even when AI takes the shortest path through it, that path has to pass through the denied logs, the reason order, and 768.

Honestly: what this still cannot catch

• The proof covers only the model, and the tests cover only the inputs they tried. So if the definition itself is wrong, both pass. Write the boundary as 1000 by mistake and the proof still holds, while the tests faithfully follow the wrong model.
• The wiring that connects the model to the real code can also be wrong. At first I passed Bend's Bool as a { $: "False" } object, and the model read logged-out as True. A red light did not mean the implementation was wrong.
• If the same AI writes both the model and the implementation, the same misunderstanding can enter both. When a proof fails, weakening the law is AI's shortest path, so it is best to have a person write LAWS.bend and hash-lock it as in the first post.
• Nothing outside the declared space can be seen. The summary goes into this limit a little further.

Summary

Adding "implement it perfectly" barely changed the result because the completion condition was still just "a button exists." So I changed what I do before handing work to AI.

1. Write down which axes the requirement is made of. Even the single line "an export button" hid the axes of login, permission, and screen width. Those axes become the space Ω, the rule each situation must keep becomes P, and what we look at to judge becomes π.
2. Check that understanding with a proof. Instead of moving on with a feeling that I had thought of everything, I prove P against a Bend model. A proof gives the same verdict on the same model every time, regardless of who interprets it. The points where the proof splits cases become equivalence partitions, and the comparison left at the end becomes the boundary value.
3. Use the proved model as the test oracle. Feed the real code partition representatives, boundary values, and random inputs, and check that it gives the same answers as the model.

Doing this caught the denied log, the reason priority, and the 768 boundary hidden in the one line "leave a log," all within the first few inputs. AI still takes the shortest path. Now that path only ends when it reaches "keeps the written laws across the whole declared space."

The remaining problem: who decides the space?

The proof shows that no input inside the declared Ω breaks P. But it cannot see outside Ω. "What if the user clicks again while exporting?" was that kind of case. The original space had no time axis for progress, so neither the proof nor the tests asked the question. Cases like this are found through reports or exploratory testing, and then the axis has to be added, as in Ω₁ = Ω × {idle, exporting}, and the laws written again.

We can prove that the laws hold inside the space. Whether that space covers enough of the situations I wanted cannot be proved formally, because the thing to compare against is a person's intent. Brian Cantwell Smith pointed out the same limit in 1985. Software engineering calls the first verification and the second validation.

So the hard work left to people sits before the proof: deciding which axes to split the problem into, how to convey those axes so AI understands them the same way, and whether ambiguous natural language like "leave a log" can be unpacked into axes and laws that match what I meant. Writing code will increasingly be AI's job, and checking that it was written right will belong to proofs and tests. I suspect a developer's work will then shift toward deciding what "right" means.

Next time you hand a feature to AI, write three things before "make it perfect": what situations exist, what must hold in each of them, and what you will look at to check.

References

These are the sources for the tool behavior and claims used in the post. The example contract, logging policy, and completion-condition format are design proposals from this post.

Bend

• bendlang/bend — README — law/proof structure, no proof search, and the --verdict kernel
• bendlang/bend — GUIDE.md — LAWS.bend/PROOF.bend convention, writing match and proofs, and calling JavaScript with -o .mjs

fast-check

• What is Property-Based Testing? — input generation, seeds, and shrinking
• User definable values — why examples run before random values

Test design

• ASTQB — 4.2 Black-Box Test Techniques — equivalence partitioning and boundary-value analysis

Limits of verification and requirements

• Brian Cantwell Smith (1985), The Limits of Correctness — the argument that proofs reach only the relation between program and model, not between model and reality
• Barry Boehm (1984), Verifying and Validating Software Requirements and Design Specifications — the distinction between verification (building it right) and validation (building the right thing)
• Pamela Zave, Michael Jackson (1997), Four Dark Corners of Requirements Engineering — requirements as statements about the outside world, satisfied by a specification only together with assumptions about that world
• Edsger W. Dijkstra (1970), Notes on Structured Programming (EWD249) — testing can show the presence of bugs but never their absence
• Bowen Alpern, Fred B. Schneider (1985), Defining Liveness — properties as conditions on whole execution sequences, split into safety and liveness
• Cosler et al. (2023), nl2spec: Interactively Translating Unstructured Natural Language to Temporal Logics with Large Language Models — using LLMs to translate natural-language requirements into temporal logic, fixing ambiguous parts interactively with a person