The README is the pitch; this is the shape of the language and why.
Haec writes and type-checks programs and emits Trope IR. It does not decide acceptability and it does not define the vocabulary. Turing-completeness lives in Haec’s terms; decidability lives in the checker’s grade algebra; they never meet. This separation is the whole point — the trust guarantee must be about the IR, not about Haec.
-
design/grammar.ebnf— a small surface: term formers,fix, the five atomic effects (attenuate,predicate,drop,sever,fuse) and the sugar (preserve,project,collapse,detach). -
design/elaboration.adoc— each construct → a Trope IR edge with its grade, and each construct’s lowering-correctness obligation (calculus O2). The sugar expands per the calculus (collapse = predicate ▷ drops;detach = drops ▷ sever).
examples/ is the executable check on the design: each .haec is paired with the
.ir.json it lowers to, and that IR round-trips through the checker.
Grades are checked against declared loss-signatures at every recursive (fix)
and effectful boundary, and inferred through the straight-line fragment. An
unbounded lossy recursion has fidelity grade top — the honest "unknown" — which
any demanding use-model rejects. The author writes the signature; Haec checks it.
This is a design pass (HC-5: small verified increments, no fluent code outrunning
its proofs). The grammar + elaboration + round-tripping examples pin the language’s
meaning before a parser/codegen exists. compiler/ and lsp/ are scaffolded
with STATUS.adoc as named future work; the runtime needs only a Turing-complete
target and is otherwise unconstrained at this stage.
There is no surface syntax for value-falsification, mis-binding, or untagged merge
(HC-3). fuse requires a tag. A buggy lowering that emitted a deceptive grade would
produce malformed IR that the checker rejects at validation — the conflation
detector at Haec’s lowering boundary.