Specify the outcome.
Describe valid inputs, required behavior, and permitted effects. Make the acceptance contract explicit.
Types as specificationsA LANGUAGE EXPERIMENT / 0.2 NextType
NextType
TypeScript that proves it.
Agents write the code.
The compiler checks the contract.
Humans review the spec.
For humans
curl -fsSL https://nexttype.dev/install.sh | shFor agents
npx skills add scrumsdotcom/scrums --skill nexttypeTHE INVOICE CONTRACT / TWO VIEWS↘
one contract / two views
type Total<xs> = { t: Int; ok: t == sum(xs) };
function total(xs: Vec<Int>): Total<xs> {
return { t: sum(xs), ok: refl };
}What a human reviews.
∀
THE SPEC / A DEPENDENT TYPE
The total equals the exact sum of its lines.
Ready to check this input2 × 6000 = 12000 minor units
RUNTIMEBrowser fixture check. The compiler and formal checker are planned.
01 / One contract, two viewsToggle the view. Change an input.
NEW INTERFACE.
ESTABLISHED FOUNDATIONS.Martin-Löf 1970s+Lean 4+Idris 2+TypeScriptExplore the research
ESTABLISHED FOUNDATIONS.Martin-Löf 1970s+Lean 4+Idris 2+TypeScriptExplore the research
01 / THE SHIFT
Build around intent.
Give agents less to guess.
Source is only one part of the work.
The contract carries the meaning.
The evidence makes the result inspectable.
Generate the change.
Give an agent typed holes and compact patches. The approved contract stays fixed: requirements, authority, and assumptions.
The agent interfaceInspect the evidence.
See which obligations were checked, which assumptions remain, and exactly which program the result describes.
Understand the proof boundaryInstall / preview CLI
One command.
Three habits.
The nt preview CLI prints a guide for agents and checks an obligation ledger. It does not compile NextType.
Read more: the CLI docs The source: Scrumsdotcom/scrums/nexttype
Install / preview CLIDesign preview — no compiler
$ curl -fsSL https://nexttype.dev/install.sh | sh$ npm install -g @scrums/nexttypeFor agents
$ npx skills add scrumsdotcom/scrums --skill nexttypeInstalls the NextType agent skill for Claude Code, Codex, Cursor, and other agents. The skill installs nt and gives the agent the three habits below.
- 01Run
nt guide. It prints the two views, how to write a contract, and where the docs are. - 02Keep obligations in
PROOF.md. Start one withnt proof init. - 03Run
nt proofbefore committing. An open obligation fails the check.
Design preview — no compiler; nt proof checks the obligation ledger format only. Verify the binary with nt.sha256 or read install.sh first.
02 / FOR AGENTS
Fixed intent.
Autonomous repair.
Agents implement, prove, test, and repair inside an approved contract.
Changed guarantees require independent owner approval.
The approval envelope sits outside the patch.
Explicit obligation
Identify the precise condition that remains unresolved.
Relevant context
Return local types and dependency references with a bounded payload.
Honest results
Distinguish a validated counterexample from an unsuccessful proof attempt.
Read more: agents and application targets The machine protocol
03 / EXECUTION
Terms. Obligations.
Execution.
Terms → obligations → execution IR → effects.
UI, API, data, and jobs consume checked operations through explicit adapters.
ONE CHECKED TERM GRAPHinvoice.core
→Terms · obligations · effects
PROPOSED COMPILER PROJECTION
c0 (sig t Z (= t (sum xs)))
f0 (pair (sum xs) refl)
put f0 c0 @b0Typed nodes and approved contracts define meaning.
Architecture proposal. The compiler and target adapters are planned.
Read more: the proposed compiler path Generated targets and their boundaries
04 / EVIDENCE
A result should show
its working.
Inspect what was checked, which version was checked, and the assumptions behind the result. A proof checks a specification. The specification still needs to express the right intent. Runtime boundaries still matter.
Read more: evidence and approval05 / BENCHMARKS
Fewer tokens.
For the whole change.
The hypothesis is simple: smaller context, precise feedback, and reusable evidence can reduce agent work.
The targets: 50% fewer tokens, 30% less elapsed time and a 50% lower escaped-defect rate. No benchmark has run.
Read more: the benchmark designTHE PRIMARY METRICNOT MEASURED
Tokens per
accepted change↘
all model tokens, including failed attemptsaccepted changes
06 / RESEARCH
Old ideas.
A different interface.
Dependent types are not new. Per Martin-Löf developed intuitionistic type theory during the 1970s.
The experiment is how agents use them to build and change executable software.
07 / STATUS
An experiment,
in the open.
Three browser fixture checks and the nt preview CLI exist today.
The language code and proof pipeline shown here are proposals.
| Stage | Deliverable | State |
|---|---|---|
| 01 | Restricted typed IR and formal semantics | Planned |
| 02 | Lean proof integration and evidence binding | Planned |
| 03 | Approval envelopes and autonomous repair controller | Planned |
| 04 | Invoice application and runtime adapters | Planned |
| 05 | Paired token and correctness benchmarks | Not measured |
START WITH ONE CONTRACT