bang v0.1.1

Native bang runner for x86_64-linux (glibc + libgcc_s only; see the install line in the README). Install: curl -fsSL https://raw.githubusercontent.com/phibkro/bang/v0.1.1/tools/install.sh | sh

Full Changelog: v0.1.0...v0.1.1

bang v0.1.0

bang v0.1.0 — a language whose paradigm and runtime are values, over a formally verified kernel.

The kernel is five primitives (thunks · force · effect rows · handlers · STM) mechanized in Lean 4; everything else — mutability, exceptions, recursion, transactions — is library code over it. Programs are descriptions until forced with $; a function's paradigm is its effect row; a program's runtime is the handler installed at the use site. Every execution path is either the verified reference or differentially tested against it: 16 headline theorems axiom-clean at {propext, Classical.choice, Quot.sound}.

The headline: a proven fast engine, as the default

bang run executes on the environment machine (ADR-0094) — its agreement with the kernel semantics is a machine-checked theorem (evalE_agrees_evalD), and it eliminates the interpreter's per-step substitution cost: the examples/json parse runs in ~50 ms where the substitution reference takes ~16 s. The reference stays one flag away (--engine=oracle) and remains the arbiter in every differential gate; --engine=compiled runs the verified calculated machine (ADR-0016).

Language

ADTs + match · generic data and bounded generics over traits (HM elaboration, monomorphized) · traits/impls with executable laws · let rec with a type-visible Div row and a structural termination checker · strings · modules v1 (import/use/pub, one file = one module, private-by-default — enforced on both access paths) · top-level declarations with main as a plain binding · -- comments · unary minus · multi-binding let x = e1; y = e2 in … (also the canonical form bang fmt emits).

User-defined effects (the moat, in progress)

effect declarations parse and type at user labels; custom dispatch is proven through the kernel, the calculated machine (Stage 4), and the binary logical relation (Stage 5, two of three arms; the third precisely characterized). The surface handle … with { … } form is Stage 7.

Tooling, agent-first

bang check --json (structured, resolver-aware, exact spans) · bang fmt (canonical, zero-config) · bang repl · bang test (law discovery, derived generators, shrinking, actionable diagnostics) · a generated reference with ~99 runnable examples · generated grammar.

Install

nix run github:phibkro/bang -- eval "1 + 2" (hermetic) · curl -fsSL https://raw.githubusercontent.com/phibkro/bang/main/tools/install.sh | sh · or the attached binary (built, stripped, and container-smoked on stock ubuntu by CI).

Known limits, named

Failures on the default engine collapse to exit 5 (re-run --engine=oracle for the specific diagnosis; sub-classification is #79). Diagnostics for imported files use merged-source coordinates. Handlers are one-shot (by design this version). No IO effects yet (Stage 7 unblocks the prong). Fuel-bounded evaluation fails loud. Trait ops dispatch through operators only (#78).

Versioning: SemVer 2.0.0, Rust-style 0.x — minors may break, loudly. Full policy + checklist: #69.