The vocabulary
A few terms we use deliberately. Here is what they mean.
Meaning engine
A meaning engine is a compiler viewed as the thing that turns intent into a verified, running system — not just a translator from source code to machine code.
When AI generates the code, the valuable work shifts from writing to verifying. A meaning engine leans into that: it checks as much as it possibly can at compile time, optimizes aggressively, and reports what it cannot prove. The more it can establish, the less wrongness reaches production.
Semantic artifact
A semantic artifact is the unit of software in a world where generation is cheap: intent-first, structured, explicit about its effects, verifiable, reproducible, and explainable.
Source code is a lossy compression of intent — which is why we surround it with tests, docs, and assertions to recover what the author meant. A semantic artifact authors the uncompressed version directly. Code does not disappear; it demotes, the way assembly survives today as a target rather than the layer people author.
Correct by construction
Correct by construction means correctness is the load-bearing structure a program is built on, not something checked afterward.
In Haskell, you encode invariants in the type system so that illegal states are unrepresentable, and a well-typed function is effectively a proof that a transformation is valid — with the compiler as the proof checker. In the happy path there is no feedback loop to run: it was right when it compiled. The model does not need to be right; it needs to be checkable.
Runtime profile
A runtime profile is a compile-time configuration in BHC that compiles the same source under a different performance contract.
The profiles are default (lazy, GC-managed), server (structured concurrency, observability), numeric (strict, guaranteed fusion, SIMD/GPU), edge (minimal runtime for WASM), realtime (bounded GC pauses), and embedded (no GC, bare-metal). Same language, same type safety — selected with a single flag.
Manifest
A manifest is a semantic artifact given three things a source file does not carry: an identity, an evidence bundle, and a provenance.
It is a single Haskell definition, named by its content rather than by a name, that records exactly what has been checked about it and carries the signatures of who vouched for it. A .hs file is something you run; a manifest is a result you cite. It is the unit of reuse in the commons — and the point at which “the model does not need to be right, it needs to be checkable” stops being a slogan and becomes data.
We say manifest, not truth manifest. A well-typed function proves consistency with a specification, not fitness for intent — head :: [a] -> a is well-typed and still partial. “Truth” overclaims; a manifest promises something narrower and more useful: a verifiable account of what was checked, by whom, under what contract.
Manifest identity
A manifest is named by the hash of its meaning together with its contract — not by its source text.
The hash is computed over the elaborated definition (typed, desugared Core with names erased), so formatting, comments, and renaming do not change identity, and two people who write the same function get the same name. But because the same source means different things under different runtime profiles, the identity also folds in the contract: the profile, the language edition, the enabled extensions, and the dependency hashes it was elaborated against. The same definition under two profiles is two manifests, because it is two behaviors. This is the semantic-artifact thesis made literal: the unit of software is meaning under a stated contract, and that pair is its name.
Attestation
An attestation is a signed, machine-checkable claim about a manifest.
That it compiled reproducibly to a given artifact; that it passes a stated property suite; that it was reviewed, or vouched for, by a particular party. The load-bearing one is reproducibility, because no one has to be trusted for it: anyone can recompile the manifest and confirm they reach the same address. On that objective floor sits human judgment — whose review you require, whose vouch you accept — enforced as policy. Provenance you can verify rather than trust.
The commons
The commons is a shared, content-addressed namespace of manifests and their attestations.
Names are metadata over hashes: a name resolves to a hash, many names can alias one hash, and a rename is a note in the margin rather than a change to the thing. Identical definitions are stored once, and their evidence and signatures pool onto the same object. Borrowing a manifest by hash guarantees identical meaning, which dissolves the class of dependency conflicts that come from packages fighting over names. Most of all, the commons is where verification stops being per-program and becomes cumulative: a result, once established and vouched for, only has to happen once.
These ideas come together in the manifesto and the essay on the commons.