Skip to content

Home

Jump to bottom
Sasha Lopashev edited this page Jul 21, 2026 · 44 revisions

BHCP

Beyond Human-Centric Programming (BHCP) is an experiment in making intent, authority, limits, and required evidence first-class program meaning. A person states what must be true and what may happen; machines remain free to discover an acceptable execution without silently weakening the contract.

BHCP is early but executable. The repository is not claiming a complete language, planner, runtime, or SDK.

OpenAI Build Week demo

Current maturity

  • Profile-source lowering implemented: #109 and PR #154 lower canonical policy, syntax, and profile definitions into deterministic typed artifacts and one atomically validated source-local registry before custom parsing or formatting. Exact syntax/profile ancestry, mappings, formatting, type-mode strengthening, overlays, and every registered policy ancestry component fail closed when invalid. Equivalent source and canonical typed documents retain identical artifact identities and CBOR; unrelated optional policy roots are not composed merely because they share a source file.
  • Recursion and retention lowering implemented: #111 and PR #155 prove and retain direct-recursion bounds, provide a fail-closed Unit base/step gate, and lower retention into an exact state-read/candidate/CAS network without implicit authority, retry, or handle-copy semantics. The source compiler, received-IR validator, reducer, proof reconstruction, and obligation graph share the checked boundary.
  • State-graph construction implemented: #116 and PR #156 materialize deterministic ownership, borrow/share/move, conflict-invariant, retention-cell, freshness, exact authority, version/CAS, and planned-transition dependencies from validated semantic IR. Exact received-graph reconstruction rejects identity, endpoint, kind, authority, invariant, version, or freshness substitution. Persistent storage, retries, competing-writer execution, and mutation authority remain runtime work.
  • Newly implemented: the generic proof checker from #117, PR #150, and the precedence correction in #151 / PR #153 revalidates complete obligation closures, sealed reducer derivations, structural child premises, four-state evidence, policy minima, verifier authority, and exact per-execution-instance claims/items/gaps without behavior-specific proof tags. The retained reducer composes child outcomes while parent-local obligations combine under Refuted > Faulted > Unresolved > Satisfied. Execution-graph construction, planning, runtime enforcement, and final evidence-graph assembly remain roadmap work.
  • Feature negotiation reconciled: #148, PR #152, and #112 / PR #157 advertise the exact obligation-, capability-, and state-builder feature identifiers emitted by real graph artifacts, with executable checks that keep execution-graph construction, planning, runtime enforcement, and final evidence assembly unclaimed.
  • Implemented: a safe-Rust canonical-source slice; complete deterministic AST parsing for v0 type, general function, predicate, and standalone refinement definitions from #100, complete goal headers, clauses, cases, calls, quantification, and nested compositions from #101, and closed policy, waiver, syntax/profile, and derived/native extension definitions from #102; the closed v0 value/type checker from #103, including canonical forms, generic bounds, nominal/structural subtyping, candidate-bound refinements, exact numerics, closed references, and recursive checked Dynamic boundaries; the complete total-pure S5 wire expression and pattern calculus from #104, including immutable construction, exact and checked numeric operations, exhaustive matching, casts, collections, and finite quantification; deterministic source-defined function/predicate elaboration from #105, including bounded generic specialization, alpha-normalized bindings, canonical verifier configuration, and fail-closed retained-call resolution; pre-IR ownership/resource analysis from #106, including exact handle qualifiers and lifetimes, move/borrow/share crossings, topology-aware concurrency, affine/linear joins, persistent-retention checks, and canonical runtime handle references; effect/authority analysis from #107, including deterministic possible-effect rows, child propagation, typed resource projection, deny-wins ceilings, policy-scoped authority, unsafe/foreign evidence gaps, direct exact limits, compatible preference groups, and retained-IR revalidation; derived/native extension resolution from #110 and PR #145, including total-pure checked lowering, reducer specialization and bound checks, exact must-understand native retention, semantic identity, and adversarial retained-IR validation; the shared typed graph identity, validation, deterministic encoding, and inspection boundary from #113; complete deterministic structural-obligation graph construction from retained semantic IR from #114, including requirements, guarantees, retained invariants and cases, verifier bindings, discharge dependencies, and exact effective-policy requirement/evidence/limit obligations; deterministic capability-decision graph construction from #115, including exact request/resource projection, authored and policy ceilings, deny-wins context, waiver provenance, required unsafe/foreign/unsupported gaps, and one validated allow decision per execution-eligible effect; and deterministic state-analysis graph construction from #116. Typed canonical AST and semantic IR, deterministic CBOR, SHA3-512 algorithm-tagged identities, CDDL validation, the minimal reducer kernel, self-hosted goal algebra, generic proof checking, the contract-bounded verifier path, policy/waiver/profile governance, and the machine-checked practical-v0 completion contract remain executable foundations. The whole-source and cross-graph audits are complete through #112 / PR #157 and #118 / PR #160; planner budget/retry allocation, execution graphs, runtime enforcement, and complete execution remain roadmap work.
  • Measured: the Phase 2 audit classifies six pilots, four multi-seed attempts, and one registered-evidence forward run without retroactive promotion. The hardened registered results are valid negatives: 0/5 contextual-policy candidates and 0/1 in-session-evidence candidates accepted. The later preregistered studies also returned null results: positive registered-adapter use and acceptance were 0/12 in #92, while both prose and BHCP arms accepted 0/12 in #93; all 24 comparative claims were conservatively calibrated. These small, single-model studies support neither an advantage nor equivalence.
  • Roadmap: Phases 1–4, the separate evidence-generalization milestone, and the fast required-CI milestone are reviewed, merged, and closed. #97 cut protected test feedback from 38:01 to about five minutes without dropping a target; PR #143 completed its full hosted matrix in about three minutes. In the open v0 — End-to-end constrained execution milestone, the frozen completion contract through effect/authority analysis #99–#107, policy/waiver, profile-source, extension, recursion/retention lowering, and the canonical source-to-IR audit #108–#112, the shared typed graph foundation, obligation/capability/state builders, generic proof checking, and cross-graph audit #113–#118, the proof precedence correction #151, and exact graph-builder feature negotiation #148 are reviewed and merged. Planner entry issue #119 is now unblocked; runtime/evidence work retains later native blockers. BHCP v0 remains incomplete until the remaining implementations and their evidence are reviewed and merged.

Start here

The repository remains the source of truth: README, vision, normative semantics, CDDL bundle, and conformance catalog.

BHCP

Canonical sources

Clone this wiki locally