Curry-Howard is All You Need

On treating user intent as propositions, code as proof, and the type checker as your verification engine

The Correspondence

In 1969, Haskell Curry and William Alvin Howard independently noticed something profound: propositions in logic correspond directly to types in programming. A proof of a proposition corresponds to a program of that type. Verification is type-checking.

Propositions  ≅  Types
Proofs        ≅  Programs
Verification  ≅  Type-checking

You may have heard this briefly mentioned in your programming language theory courses. Today I'm arguing it's the missing piece in how we build software.

If user assertions are propositions, and we can compile them into types, then code that type-checks is provably correct against those assertions. The compiler becomes your verification engine. Tests become property checks derived from type invariants.

Intent as an Assertion Tree

Here's the first insight: user intent is a tree of increasingly specific assertions.

"Users can manage tasks"
├── "Users can create tasks"
│   ├── "Tasks have a title (required, 1-200 chars)"
│   ├── "Tasks have a description (optional)"
│   ├── "Tasks are created in 'pending' state"
│   └── "Creating a task fails gracefully if storage is full"
├── "Users can complete tasks"
│   ├── "Completed tasks show a timestamp"
│   ├── "Completion is reversible"
│   └── "Completing already-complete task is a no-op"
└── "Users can delete tasks"
    ├── "Deletion requires confirmation"
    ├── "Deleted tasks are soft-deleted for 30 days"
    └── "Users cannot delete tasks they don't own"

The root should be vague because it's more abstract and more general, but the leaves should be precise enough to test. Every node is a proposition that can be confirmed or denied. Child nodes elaborate on parent nodes.

The Pipeline

┌─────────────────┐
│  User Intent    │  "Build a blog where users can write posts.
│  (natural lang) │   Only authors can edit their own posts."
└────────┬────────┘
         │ LLM generates
         ▼
┌─────────────────┐
│   Assertions    │  ← User confirms/denies
│   (structured)  │
└────────┬────────┘
         │ Compile
         ▼
┌─────────────────┐
│  Type Schema    │  ← Zod / TypeScript types
│  (formal spec)  │
└────────┬────────┘
         │ Derive
         ▼
┌─────────────────┐
│  Property Tests │  ← fast-check / vitest
│  (verification) │
└────────┬────────┘
         │ Synthesize
         ▼
┌─────────────────┐
│  Implementation │  ← Must satisfy types
│  (proven code)  │
└─────────────────┘

Each stage acts like compilation step and each output is more formal than the input. The key here being that each stage has a verification mechanism that doesn't require human judgment.

Stage 1: Structured Assertions

Raw assertions are prose but prose doesn't compile. The first step is giving assertions structure:

type StructuredAssertion = {
  id: string;
  naturalLanguage: string;
  formal: AssertionFormal;
};

type AssertionFormal =
  | EntityAssertion // "Users exist in the system"
  | PropertyAssertion // "Email must be valid format"
  | InvariantAssertion // "Balance is never negative"
  | PreCondition // "Only authors can edit"
  | PostCondition // "After creation, record exists"
  | RelationAssertion; // "Posts belong to Users"

An LLM can generate these from natural language. We ask the user to confirm or denies each one. Every confirmation adds a constraint to the system, every denial removes one.

Here's what "Only the author can edit a post" looks like as a structured assertion:

{
  id: '4',
  naturalLanguage: 'Only the author can edit a post',
  formal: {
    kind: 'precondition',
    operation: 'updatePost',
    requires: {
      op: 'eq',
      left: { field: 'currentUser.id' },
      right: { field: 'post.authorId' }
    }
  }
}

Now we have something we can compile.

Stage 2: Types

Assertions compile to Zod schemas and TypeScript types:

// Compiled from assertions
export const PostSchema = z.object({
  id: z.string().uuid(),
  title: z.string().min(1),
  content: z.string(),
  authorId: z.string().uuid().brand("UserId"),
  createdAt: z.date(),
  updatedAt: z.date(),
});

export type Post = z.infer<typeof PostSchema>;

// From precondition assertion
export function assertCanUpdatePost(ctx: {
  currentUser: User;
  post: Post;
}): asserts ctx is typeof ctx & { __authorized: true } {
  if (ctx.currentUser.id !== ctx.post.authorId) {
    throw new AuthorizationError("updatePost", "User is not the author");
  }
}

As you can see, the precondition becomes a type guard. The type system now enforces that any code calling updatePost must first call assertCanUpdatePost.

This is Curry-Howard in action: the proposition "only authors can edit" becomes a type and code that type-checks is a proof that it respects that proposition.

Stage 3: Tests

Types give us schemas, schemas give us generators, generators give us property-based tests:

describe("updatePost authorization", () => {
  it("allows author to update their post", () => {
    fc.assert(
      fc.property(UserArbitrary, PostArbitrary, (user, post) => {
        const authoredPost = { ...post, authorId: user.id };
        return canUpdatePost({ currentUser: user, post: authoredPost }) === true;
      })
    );
  });

  it("denies non-author from updating post", () => {
    fc.assert(
      fc.property(UserArbitrary, UserArbitrary, PostArbitrary, (author, otherUser, post) => {
        if (author.id === otherUser.id) return true; // skip
        const authoredPost = { ...post, authorId: author.id };
        return canUpdatePost({ currentUser: otherUser, post: authoredPost }) === false;
      })
    );
  });
});

These tests are derived, not written. If the implementation passes the type checker and these tests, it satisfies the assertion implied by the proposition.

Stage 4: Code Synthesis

Now we synthesize implementation with executable verification in hand. The LLM must produce code that:

Imports the generated types (cannot redefine them)
Passes the generated tests (cannot skip them)
Calls the assertion guards (compiler enforces this)
Validates against schemas (runtime enforcement)

export async function updatePost(
  currentUser: User,
  postId: string,
  input: { title?: string; content?: string }
): Promise<Post> {
  const post = await db.post.findUniqueOrThrow({ where: { id: postId } });

  // REQUIRED by type system - compiler error if omitted
  assertCanUpdatePost({ currentUser, post });

  const updated = PostSchema.parse({
    ...post,
    ...input,
    updatedAt: new Date(),
  });

  await db.post.update({ where: { id: postId }, data: updated });
  return updated;
}

The verification loop continues until the code proves it satisfies the assertions.

The Feedback Loop

What happens when tests fail?

If code fails a test derived from Assertion A, there are two possibilities:

The code is wrong (LLM regenerates)
Assertion A contradicts reality or other assertions

The second case is actually key to this process, the system surfaces it to the user:

"Your assertion 'Users can share documents with anyone' conflicts with your earlier assertion 'Documents are private by default'. Which should change?"

Contradictions in requirements are caught before anyone writes real code. This means we are using the type system like a requirements debugger.

Logical Propagation

Assertions have logical relationships:

A → B   (implication)
A ∧ B → ⊥   (contradiction)
A requires B   (dependency)
A ⊕ B   (mutual exclusion)
A ↔ B   (equivalence)

When a user confirms assertion A:

Everything A implies becomes true
Everything contradicting A becomes false
Everything A depends on must be addressed

When a user denies assertion A:

Anything requiring A is now blocked
Parent assertions that entailed A need revision

This is constraint propagation over the assertion graph, achieved automatically through the type checker. A single "yes" or "no" can ripple into dozens of inferred conclusions but the system maintains consistency automatically.

Traceability

You could even go as far as to trace every line of generated code back to an assertion:

// @assertion-id: 4
// @assertion: "Only the author can edit a post"
// @derived-type: assertCanUpdatePost
// @derived-test: "denies non-author from updating post"
assertCanUpdatePost({ currentUser, post });

This enables queries that are usually impossible:

"Which assertions does this code implement?" → Read annotations
"Which code implements this assertion?" → Grep for assertion ID
"What breaks if I change assertion X?" → Recompile, see what fails

Because this is generated by an LLM, it could be fully automatic with no maintenance burden.

What This Unlocks

If intent is a formal logical structure:

Diffing intents becomes diffing trees. You can compute exactly what changed between versions of requirements.

Merging intents from multiple stakeholders becomes tree merging with conflict detection. Product wants X, engineering wants Y—where exactly do they conflict?

Intent coverage can be measured like code coverage. What percentage of your assertions have corresponding tests? What percentage have implementation?

Intent debt (vague or missing assertions) can be tracked like tech debt. You can see which parts of your system are under-specified.

Intent refactoring (restructuring the tree without changing meaning) becomes a thing. Clean up your requirements without changing behavior.

The Vision

Most software is written with an implicit, partial, inconsistent assertion tree that exists only in people's heads. Bugs happen when:

Assertions conflict (nobody noticed)
Assertions are missing (nobody thought about it)
Code violates assertions (implementation error)
Assertions don't match actual user intent (requirements error)

The idea is an agent that maintains an explicit assertion tree, keeps it in sync with user intent, and verifies code against it.

The type checker would automatically tell us that the code matches the spec. We wouldn't need to trust that requirements are consistent, constraint propagation would verify it automatically. We wouldn't need to assume we understood what the user wanted, the assertion tree would make our understanding explicit and falsifiable.

The Key Insight

Requirements verification is fundamentally about making implicit assumptions explicit.

Logical encoding surfaces contradictions.
Precondition inference surfaces dependencies.
Type checking surfaces ontological assumptions.
Tests surface behavioral assumptions.

Code is just the lowest level of the assertion tree. A function is an assertion that "when called with X, Y happens." Tests are assertions made executable. Types are assertions checked at compile time.

The Curry-Howard correspondence is the bridge between what humans want and what machines can verify.

Propositions are types, proofs are programs. The question "does this code do what the user wanted?" has a mechanically verifiable answer.

Curry-Howard is all you need.

Andrue's Lab