Purpose

Purpose

The problem

Mainstream programming languages are optimized for humans to prescribe procedures. Coding agents can generate those procedures quickly, but prose tickets, source code, policy, and evidence often remain separate—and a plausible implementation can quietly satisfy the visible tests while changing the intended meaning.

BHCP explores a different contract: declare outcomes, authority, limits, effects, preferences, and acceptance evidence in one typed semantic model. An implementation may choose how to achieve a goal, but it must not erase obligations, invent authority, or claim acceptance without the named evidence.

Who it is for

• People and organizations delegating consequential work to coding or execution agents.
• Tool builders who need deterministic intent artifacts, stable identities, and independently checkable evidence.
• Language and verification researchers testing whether semantic contracts improve correctness and claim calibration.

Proposed value

The project is trying to make four properties executable:

1. Intent survives representation changes. Formatting, comments, labels, and safe custom layouts do not change semantic identity.
2. Authority only narrows downward. Organization, team, repository, and user policy layers compose monotonically; a later layer cannot casually weaken an earlier one.
3. Behavior grows outside the trusted core. Standard goal algebra is checked-in BHCP prelude source over a tiny behavior-neutral kernel.
4. Completion is evidence-bound. “Implemented,” “verified,” and “accepted” are different states, and operational faults are not disguised as semantic rejection.

These are design commitments and active implementation targets—not proof that BHCP is already objectively superior to Python, TypeScript, Rust, or other general-purpose languages.

The first property is now demonstrated by a checked-in symbolic layout and a spaced narrative layout for the same policy-governed goal. They retain different profile, comment, label, formatting, AST, and IR artifact identities while sharing the same resolved overlay and semantic identity. A meaningful overlay change breaks that equivalence, so the evidence distinguishes presentation freedom from policy changes. The Phase 4 completion audit binds three acceptance claims for each issue #41–#49 to named checked-in tests and verifies the evidence links and explicit non-goals. This completes the bounded presentation milestone without claiming a complete BHCP v0.

The Phase 2 completion audit makes the same distinction for coding-agent evidence. Historical pilots remain replayable artifact records, invalid and excluded controller runs retain those classifications, and the two hardened registered model studies remain valid 0/5 and 0/1 negatives. The exact adapter integration accepts the focused candidate, but the later positive-use study #92 observed 0/12 registered use and 0/12 acceptance. The paired comparison #93 observed 0/12 acceptance in both prose and BHCP arms and 12/12 conservative claim calibration in both arms. The reviewed preregistration #91, all 36 sessions, exclusions, usage, and exact analyses are retained. These null results do not establish equivalence or a broad BHCP-versus-prose effect.

Success measures

• Canonical and presentation-varied sources lower to deterministic, schema-valid artifacts with the expected identity invariants.
• Standard behaviors are self-hosted without new behavior-specific Rust primitives.
• Layered policy rejects every unauthorized weakening with stable diagnostics.
• Coding-agent evidence records pin their reproducible boundary, distinguish historical replay from hardened registration, and remain honest about ties, overhead, variance, exclusions, and failures.
• Registered adapters can move an exact obligation from source to independently accepted evidence without adding manifest authority; the completed 0/12 study did not observe model use of that path.
• Practical v0 completion additionally requires the complete normative source surface to reach checked semantic IR, deterministic obligation/capability/state/proof graphs, a valid explained plan, capability-bounded execution, exact result states, and independently checkable per-obligation evidence through the safe-Rust SDK and CLI. #99 freezes that target as a machine-checked reference contract and program. #100 completes type/function/predicate/refinement parsing, #101 completes goals and composition, #102 completes closed governance/profile/extension definitions, #103 completes the closed value/type/refinement boundary, #104 completes the total pure v0 wire expression and pattern calculus, #105 completes deterministic function/predicate elaboration, #106 completes pre-IR ownership/resource analysis, #107 completes possible-effect propagation and authority boundaries, #109 completes profile-source lowering, #110 completes derived/native extension resolution and lowering, #111 completes the bounded direct-recursion and handle-free retention-prelude slice, #112 completes the whole-source governed-IR audit, #113 provides the shared typed graph validation and identity model, #114–#117 implement obligation, capability, state, and complete-obligation proof analysis, and #118 completes their cross-graph consistency audit. Execution-graph planning, runtime enforcement, and final evidence assembly remain explicit later stages in milestone 7. The end-to-end product is not yet an implemented claim.

Non-goals for the current roadmap

• A distributed executor, unrestricted agent backend, or execution authority not explicitly granted by the checked program and effective policy.
• Arbitrary grammar plugins, macros, parser callbacks, or profiles that can change core meaning.
• Treating hidden tests as semantic authority or using a skill as a second language specification.
• Claiming broad productivity or correctness advantage from a small number of intentionally narrow pilots.

Read the vision for the long-term product direction and SEMANTICS for normative v0 behavior.