Today I’m tagging bb.scm v0.1.0 — the another release of the Möbius, a Chez-Scheme implementation of a content-addressed programming language where code identity is structural, not nominal. Same algorithm in Tamazight, Arabic, French, English → identical SHA-256 hash, after de Bruijn normalization. Names are mappings. The hash underneath is the same.
The full design lives in manual.md.
v0.1.0 is the part of that design that runs.
The language (R⁰RM, Part II). A tree-walking
interpreter for the 39 foundations and the one mechanism —
gamma, the catamorphic pattern-matching combiner. The
reader, the de Bruijn normalizer, the pattern matcher, the environment
frames, capsules, boxes, lambda, guard/continuation foundations, and a
base library written in Mobius itself. SHA-256 in pure Scheme so
identity is reproducible without external dependencies.
The store (Part III, partial). Append-only content
store on the filesystem: combiners/<sha256>/tree.scm
for the immutable normalized AST,
mappings/<hash>/map.scm for per-language
presentation, plus lineage, worklog, and review marks.
bb add parses, normalizes, hashes, and stages.
bb commit promotes WIP to committed.
bb refactor propagates a hash substitution through a
dependency tree. bb diff does a structural compare with
ANSI colors. bb validate re-hashes the whole store.
The toolchain (Part IV). Most of bb’s
command surface from §29 of the manual:
add, edit,
commit, refactorcheck, review,
validate, diffshow, search,
tree, caller, resolve,
log, statuseval, run,
repl, printremote add/list/remove/push/pull/sync,
remote publish/stopstore init,
store info, worklog,
mapping list/set/deleteA runtime around the language. A small
transparent runtime (io_uring HTTP server/client) ships
alongside, so combiners can be served without leaving the Mobius surface
— see bb serve <app-ref> <handler-ref>.
Reference syntax. A flexible
<ref> grammar — name,
name@nid, name@nid@lang,
name@nid@lang@lid — with hash prefixes (minimum unique)
accepted anywhere a hash is expected. Documented in the README and the
project CLAUDE.md.
Read the bottom half of the manual as the to-do list. Concretely:
bb prove and bb verify
(§29.8). Zero-Knowledge Proofs for sealed combiners — the
Privateer persona. The seal works (hashes can be locally
committed and OTS-anchored without disclosure); proving capability
without disclosure does not.bb search --near), behavioral indexing by check suite,
language-axis search across federated stores. Designed; not built.eval as integer->combiner hash lookup,
top-level mutual recursion, capsule type-ID derivation, parameterized
hash/anchor/proof-system, and predicate inference. These are real and
not hand-waved.The honest summary: the language and the store are usable today; the cryptographic-trust layer (ZKP + oblivious execution) and the cross-store discovery layer (Atlas Stoa) are designed but not implemented; the formal corners (effects, errors, eval) are open questions, not bugs.
Three example projects ship under examples/.
They are not toys — they exist to stress the language at the boundary
where the multilingual story has to survive contact with HTTP, mutable
state, and a real browser.
examples/counter — the
clickerA server-rendered click-counter that survives page refreshes.
Demonstrates the two-combiner server interface —
bb serve <app-ref> <handler-ref> — where
app-ref is called once at startup to build shared state and
handler-ref runs on every request. State is a single
box holding a Chez vector; mutation is box!.
The interesting part is xeno: the escape hatch from Mobius
into Chez. It’s there, it’s necessary at the I/O boundary, and the
design pressure is to keep it small.
examples/todomvc
— the canonical exerciseTodoMVC, but as Mobius combiners served by the same
bb serve runtime. Eight combiners — todos,
todos-state, todos-toggle,
todos-delete, todos-remove-completed,
todos-count-active, todos-render-list,
todos-render-item — composed by hash, deployed as one
process. The HTTP request/response shape is an alist of strings, the
state is (cons next-id todos-list), and the handler
dispatches on method + action query param. It
exists because TodoMVC is the lingua franca of “is your stack real?”
examples/invariant
— the trilingual blogA full static site generator written in Mobius — trilingual
en/fr/es — generating the Invariant blog.
Thirty stories per language. The user-facing combiners share a hash
across language mappings: generate / engendrer
/ engendrar, render-post /
afficher-recit / mostrar-relato, and so on.
The xeno surface is two files, both in
src/io/. Everything else — list traversal, string
composition, HTML construction, language dispatch — is pure Mobius.
This is the example that matters most to me. It is the meta-story of
the project: the personas of the manual are recurring characters in the
fiction, the store is the fictional infrastructure, and the blog is
generated by the system the blog is about. Two real bugs in
bb were discovered and fixed during its construction
(mapping resolution order; qualified name self-reference for ambiguous
combiners). Dogfooding earned its keep.
git clone https://github.com/amirouche/bb.scm
cd bb.scm/north
./bb replOr evaluate the abacus from the README — six clauses of catamorphic arithmetic — in three languages, three identical hashes:
(define abacus
(gamma
(("num" ,n) n)
(("add" ,(a) ,(b)) (+ a b))
(("sub" ,(a) ,(b)) (- a b))
(("mul" ,(a) ,(b)) (* a b))
(("neg" ,(a)) (- 0 a))
(("do" ,(r)) r)))The recursion is in the commas. The identity is in the hash.
A check is a combiner that takes the combiner under test as its
argument. bb check applies the check to the candidate;
assume decides pass/fail.
Hard-coded check — concrete inputs, concrete expected outputs. Useful for base cases and regression tests:
(define ~check-abacus-base-cases
(lambda (abacus)
(begin
(assume (= 7 (abacus (cons "num" (cons 7 #nil))))
"literal 7 evaluates to 7")
(assume (= 5 (abacus (cons "add"
(cons (cons "num" (cons 2 #nil))
(cons (cons "num" (cons 3 #nil)) #nil)))))
"2 + 3 = 5")
(assume (= -4 (abacus (cons "neg"
(cons (cons "num" (cons 4 #nil)) #nil))))
"neg of 4 is -4"))))Three concrete trees, three concrete answers. Run
bb check abacus and it prints PASS /
FAIL per assumption.
Symbolic check (Z3) — return a lambda instead of
calling assume directly. Its parameters become Z3
variables, its body becomes an SMT assertion, and the combiner under
test is inlined as a define-fun. The property is verified
universally over the parameter domain, not on a finite witness set:
(define ~check-double-is-times-two
(lambda (double)
(lambda (x)
(assume (= (double x) (* 2 x))
"double(x) = 2 * x for every integer x"))))When z3 is on PATH, bb check
reports Z3-PASS (the SMT solver found no counterexample) or
Z3-FAIL with the offending value of x. When
z3 is missing, the same combiner returns
Z3-SKIP and the rest of the suite still runs — symbolic
checks degrade gracefully into “not verified here.”
The two styles compose: a check suite typically pins specific corner
cases by hard-coding and proves the general invariant symbolically. The
check suite is the specification — content-addressed, forkable,
translatable into Tamazight or French, and (eventually, when
bb prove lands) the statement a Zero-Knowledge Proof would
attest to without disclosing the implementation.
First release of bb.scm — a CLI for Möbius with Chez Scheme
Content-addressed “Scheme”: write code, get a hash, the same hash across French, English, Tamazight, Arabic, and Mandarin.
git clone https://github.com/amirouche/bb.scm
cd bb.scm && make
./bb --help
Feedback welcome.