Skip to main content
Synthesize code from a specification | ESSThe synthesis plan, the four targets behind it, obligations as the contract with the human, and how the generated code is proven against the generated suite.ESShow-toesshow-toadopterdevelopertry-spec-driven-developmentspecify

Synthesize code from a specification

Structural synthesis generates the part of an implementation that was never yours to write — types, typestate lifecycles, component ports, one transport — and hands back everything it will not guess as a named obligation. Behaviour is never generated: every algorithm is an obligation someone implements.

$ ess generate synthesize --path examples/billing --target rust --out out/

--target is rust, go, web or clap; --out writes the tree, and without it the artifacts are listed instead of written, for the same reason ess generate behaves that way — a verb that scatters files over a working tree the first time someone tries it is a verb nobody tries twice.

The plan: every capability gets exactly one disposition

Synthesis starts with a language-neutral synthesis plan. Every capability of the specification receives exactly one of three dispositions, with the reason recorded:

DispositionMeaning
generatedthe specification determines it fully; the emitter writes it
obligationthe specification cannot determine it — a decision or an algorithm — so it is named and left to a person, with a declared seam to implement against
refusedthe specification cannot even state what would be needed; the reason is printed

The command summarizes the plan and the artifact inventory. PLAN.md and plan.json in the output carry each disposition and its reason:

$ ess generate synthesize --path examples/billing --target rust | head -2
48 capabilities: 36 generated, 8 obligation(s), 4 refused
15 artifact(s), nothing written

A refusal reads the same way and says what it cannot state: "actor grants billing.invoice.Auditor — a grant is checked against a caller identity, which types do not carry".

The plan is rendered as PLAN.md and plan.json in every emitted tree, and it is language-neutral. The existing Rust, Go and Web billing example produces the same 48/36/8/4 summary and plan.json digest. Clap also carries the plan and reports its grammar-specific weakenings separately; command behavior remains a handler obligation.

What a target holds more weakly or cannot represent at all is declared in a TARGET.md beside the plan — a named weakening, never a silent downgrade. The Rust target is the one the others are measured against and emits no such file; Go's names four weakenings and the browser's six, each with the capabilities it touches. The browser tree's first row is the worked example: it cannot carry #![forbid(unsafe_code)], because a WebAssembly export is a #[no_mangle] item and rustc's own unsafe_code lint flags one. The file says so, states that the crate contains no unsafe block, no unsafe fn and no raw-pointer dereference, and a test asserts the property the lint would have closed. What is lost is the compiler closing the question, not the property.

The four targets

TargetEmitsDependencies
rusta cargo workspace: semantic types, typestate lifecycles, component ports, one HTTP transportnone
goa Go module with the same systemstandard library only
weba WebAssembly bridge over the Rust target plus a page built at load time from an emitted catalog.json — no model is typed into its HTMLno build tool, no wasm-bindgen
clapa command tree, shell completion support and a dispatcher with Handler seams for components declaring command-line reach and a CLI grammarclap and clap_complete 4

Clap emits grammar rather than another type layer. Its handlers receive clap::ArgMatches; the unimplemented handler names the obligation and refuses. The generated dependencies support parsing and completion, so the Rust target's zero-dependency boundary does not apply to Clap. See the Clap emitter and handler/completion tests.

All four full synthesis targets refuse unsupported modeled Binary64, as covered by the feasibility tests. This boundary is separate from the structural data libraries. The support matrix records current-source target availability independently of the dated release observation.

examples/gatepass/ is emitted to Rust and Go and deliberately not to the browser: it is a component whose own words say its callers are not deployed with it, and a surface reached over a network is one a page would call rather than contain.

Realizations: the human's half

An obligation is implemented in a separate, hand-written crate or module — a realization — that plugs into the generated seams. Three ship here: examples/billing-realization/, examples/gatepass-realization/ and examples/gatepass-go-realization/, one implementation per obligation in the generated plan, linked into the generated tree. The linker never chooses between candidate implementations; ambiguity is an error.

How the output is proven, not assumed

The generated code is judged by the suite the same specification generated (see Verify an implementation), and the repository's task check gate runs the source-workspace tests and realization checks on every commit. Use the public ess generate synthesize command to write a target and review its output:

  • The committed billing suite, unchanged, passes the generated workspace linked with the hand-written realization — 29 of 29 scenarios — and a deliberately corrupted linkage fails exactly the scenario that exists to catch it.
  • Generator tests cover the structural contracts and deterministic bytes. The browser-specific task site-build gate additionally compiles the committed WebAssembly realization and runs a Node-driven boundary test that loads the module outside a browser and drives it through the page's own glue. Its last line is browser boundary: 21 claims held — catalogue, dispatch, transport, view, refusal, redelivery — the count is derived from the checks the script actually makes, not written down beside them. That gate fails when its toolchain is missing; it does not report a skipped check as passing.
  • The dual-target demonstration: examples/gatepass/ is synthesized to Rust and Go, both binaries are started on ephemeral ports, and their startup records, their answers to seven HTTP exchanges, and the /openapi.json and /docs documents they publish are compared. The seven are chosen to separate the kinds of "no": a registered visit (202), a visit of no length refused on domain grounds (422), two view reads (200), a body the schema refuses (400), an undeclared path (404) and a declared path under an undeclared method (405). The two applications must agree with each other and with the committed artifacts, byte for byte where bytes are claimed.

Where the HTTP surface comes from

The gatepass model gained exactly one word to become a running server: a component may declare reached_by: network, which states where its callers are and names no protocol. HTTP follows because the one contract this project projects for a command surface is an OpenAPI document — the transport is derived, which is the typed projection boundary doing its job.

Honest limits

  • Generated code is structural, never behavioural. Every algorithm is an obligation.
  • Obligations are plan entries, not yet artifacts a task can own and evidence can close. That extension is W7.4, and it is deferred by operator decision rather than blocked: docs/plan/ess-wave-7-closing-the-loop.md § W7.4 — deferred by operator decision records that nothing else in wave 7 depends on it and that its one precondition — a contract digest that exists in code — is now met. What closes it is scheduling it, which is a decision somebody takes, not a build somebody is waiting on. It is on the roadmap under Deferred by decision.
  • The demonstration is not a deployment: plain HTTP, no auth, no TLS, one connection at a time, no servers block because the model has no URL.