The specification

The normative reference for Halis is SPEC.md in the repository. It is the legal document of the project: the v1.0 API surface is pinned at a digest, hls-freeze refuses drift, and every amendment travels in a hash-chained ledger.

How to read it

SPEC.md is a historical document. It describes the language as it evolved, stage by stage, and it has been edited continuously since the beginning. Some of its statements describe an earlier state of the language.

Where SPEC.md disagrees with the shipped compiler, the compiler is right. Concretely, two known examples:

Where	What it says	What is true in v1.0
SPEC.md §17.1 heading	“The eight active effects”	There are nine — Conc was added in Stage 16
SPEC.md §9	“Five fine-grained effects”	The IO family still has five, but there are four more outside it
SPEC.md §3	“Move semantics & ownership arrive in Stage 8”	Ownership shipped in Stage 8 and is current behaviour

That is exactly why the quick reference on this site is generated from the compiler source rather than from the specification: the effect list comes from src/hlc/parser.hls, the builtin mapping from src/hlc/checker.hls, and the module lists from the std/ and core/ trees. When the compiler changes, the reference changes with it.

The chapters

Section	Covers
§1–§2	Design philosophy, lexical rules
§3–§4	Types, program structure, imports
§5–§8	Statements, expressions, builtins
§9	The effect system
§11–§12	Memory model, Result and the ? operator
§16	Ownership: drop, clone, take
§17–§19	Effects, capability tokens, taint tracking
§24–§27	FFI, concurrency, attributes, freestanding
§26, §52–§54	Contracts, refinement types, the proof engine

The full table of contents, with the opening line of every chapter, is generated into the quick reference.

Frozen API

tests/api_freeze.json and the hls-freeze tool pin the v1.0 surface. The make freeze-verify gate refuses drift on every commit, and hls-migrate replays every prior release’s corpus so an old tree can be upgraded without guessing.