The language where LLM edits survive.

Playground · Cheatsheet · Specification · Why · Quick start · Evidence · How it works · Status

An edit that survives

Almide is a statically-typed language built for one metric: modification survival rate — how often code still compiles and passes its tests after a series of AI-driven edits. It compiles to native binaries (via Rust) and to WebAssembly, and the two produce byte-identical output.

The metric in one screen. A model adds a case to a type and, as models do, touches nothing else:

type Shape =
  | Circle(Float)
  | Square(Float)
  | Triangle(Float, Float)   // the edit

fn area(s: Shape) -> Float =
  match s {
    Circle(r) => 3.14159 * r * r
    Square(w) => w * w
  }

error[E010]: non-exhaustive match: missing Triangle(_, _)
  --> shape.almd:7:9
  in match
  here: match s {
  hint: add arms for Triangle(_, _):
  Triangle(arg1, arg2) => _
Or use `_ => todo()` to compile incrementally.

The compiler names the missing case at the site, spells out the arm to add, and offers a way to keep compiling while the rest is written. The model's next turn is Triangle(b, h) => 0.5 * b * h; the program then runs natively and on wasm and prints the same bytes. That loop — an edit, a diagnostic that is itself the fix, a passing build — is what every decision below serves.

Why Almide?

• Predictable — One canonical way to express each concept, reducing token branching for LLMs
• Local — Understanding any piece of code requires only nearby context
• Repairable — Compiler diagnostics guide toward a specific fix, not multiple possibilities (as above)
• Compact — High semantic density, low syntactic noise

The full rationale: Design Philosophy. The frozen surface and the breaking-change policy: STABILITY.md (declared 2026-08-20) — anything in the Cheatsheet or llms.txt keeps meaning what it means.

Quick Start

Try it in your browser → — no installation.

curl -fsSL https://raw.githubusercontent.com/almide/almide/main/tools/install.sh | sh   # macOS / Linux
irm https://raw.githubusercontent.com/almide/almide/main/tools/install.ps1 | iex        # Windows (PowerShell)

The installer checks the archive against the release's almide-checksums.sha256 before unpacking. To verify a downloaded asset yourself — every release asset, the checksums file included, is Sigstore-attested by the release workflow (see SECURITY.md):

gh attestation verify almide-macos-aarch64.tar.gz -R almide/almide   # provenance: built by almide/almide's release workflow
sha256sum -c --ignore-missing almide-checksums.sha256                # digest matches the published checksums file

Each archive also carries almide-verify, the independently versioned certificate checker: almide verify app.almd emits the program's ownership / name / capability / call-mode witnesses and hands them to it (it must sit next to almide or on PATH — there is no built-in fallback).

From source, with Rust 1.94+ (the binary embeds the wasmtime host): cargo build --release && cp target/release/almide target/release/almide-verify ~/.local/bin/ (or make install).

fn main() -> Unit = {
  println("Hello, world!")
}

almide run hello.almd                 # native
almide run hello.almd --target wasm   # same bytes, on wasmtime

Features

• Multi-target — Same source compiles to a native binary (via Rust) or WebAssembly (direct emit, no LLVM)
• Generics — Functions (fn id[T](x: T) -> T), records, variant types, recursive variants with auto Box wrapping
• Pattern matching — Exhaustive match with variant destructuring
• Effect functions — effect fn for explicit error propagation: expr! propagates, a bare fallible call is an error, never silent
• Bidirectional type inference — Annotations flow into expressions (let xs: List[Int] = [])
• Codec system — Type.decode(value) / Type.encode(value) with auto-derive
• Map literals — ["key": value], m[key], for (k, v) in m
• Fan — structured concurrency: fan { a(); b() } on real threads natively, sequential on wasm; fan.map / fan.any deterministic by list order on both
• Pipeline operator — data |> transform |> output
• Module system — Packages, sub-namespaces, visibility control, diamond dependency resolution
• Standard library — self-hosted .almd modules: string, list, map, json, http, fs, and more (reference; the count is derived under Project Status)
• Built-in testing — test "name" { assert_eq(a, b) } with almide test

What is measured

Every claim in this section is either derived by a script or carries the date it was measured; scripts/check-readme-numbers.sh refuses a bare number in CI, and refuses an LLM-writability scorecard that is older than 90 days or that does not name the almide-dojo run it came from.

LLM writability

Measured by almide-dojo on 2026-09-22 across its bank of 38 tasks (basic / intermediate / advanced), with the pinned compiler almide 0.62.0, by that repo's CI lane. Both runs are stamped comparable by the harness — every planned task reached the model, so each rate is a point and not an interval — and both were sampled at a fixed seed (20260922) and temperature 0, recorded in the run's manifest as what the provider actually put on the wire. The runs are committed — almide-dojo@8af34bc — so the table below can be recomputed from their summary.md rather than believed; later runs are on the live dashboard. No Anthropic or OpenAI key is in CI by decision, so the models here are the ones the lane can reach without one:

Model	Pass Rate	1-Shot Rate
Llama 3.3 70B (fp8-fast)	65% (25/38)	39% (15/38)
Llama 3.1 8B	44% (17/38)	34% (13/38)

The most recent same-model comparison is the MiniGit bench: Sonnet 5 × 20 trials on 2026-07-15, 100% pass, the most concise of 5 languages (233 LOC), and the fastest agent wall-clock against Gleam and MoonBit — an LLM-writability number, measured under 6–9× self-parallelism, not generated-code speed (chart · method · upstream).

Byte-identical across targets

Every program that compiles for both targets produces byte-identical observable output — stdout, stderr, exit code — whether it runs as a native binary or as WebAssembly. Native is the oracle; native == wasm is a hard invariant, not a "target difference" to be documented around.

The guarantee is continuous, with an explicit, ledger-managed scope: "byte-identical" means the execution output, not the compiled artifacts; inherently nondeterministic sources certify deterministic invariants instead of exact bytes; APIs not yet implemented on wasm are compile- or run-time refusals — never wrong bytes; and exactly two fns are exempt because their job is to report the host — env.os() and env.temp_dir(), bounded by C-189, since making them agree across targets would be the defect rather than the guarantee.

This claim is not prose. Every observable promise is a named contract in the behavior-contract ledger, each traceable to executable evidence, and the numbers below are regenerated from the ledger (scripts/gen-claims.sh, enforced by scripts/check-contracts.sh in CI):

Ledger: 372 contracts — 372 active, 0 flagged-for-revision.

Divergences awaiting a fix: none. Every contract in the ledger is active, carrying executable evidence of class >= fixture. The one by-design carve-out in the law — the platform-reporting fns env.os and env.temp_dir — is bounded by C-189.

Scope, ledger mechanics, and the evidence stack (contract ledger, cross-target fixture gate, differential fuzz, emit-time Σ-probes, Lean belt, org-wide byte-verify sweep): docs/design/EQUIVALENCE.md.

Memory safety — proven where it is proven, trusted where it is trusted

You write no ownership annotations, no lifetimes, no free: Perceus-style ownership inference in the compiler decides where every heap value is introduced, duplicated, and consumed — garbage-collector-free, pause-free. The checker for those decisions is kernel-proven (Rocq/Coq spine, 99 audited theorems and lemmas, axiom-clean, independently re-checked by coqchk; the count is asserted by proofs/check.sh), and almide verify --emit still produces the MIR ownership witness it checks. The per-build certificate used to ride the incumbent wasm leg, which #2761 deleted; the structural wasm leg (the only wasm renderer) and the native leg are trusted, certificate pending (#2755–#2760): their evidence is differential — byte-identical output against each other and the interpreter on the contract corpus, held by a grow-only floor and a semantic-mutation net — and the structural runtime's bytes are checked against the Coq decoder model by proofs/check-structural-bytes.sh. The boundary, stage by stage: proven-vs-trusted.md; the full account, including the Lean 4 Perceus belt the design started from: docs/design/MEMORY-SAFETY.md.

Performance

No runtime, no GC, no interpreter — native compiles through Rust to machine code, and WASM is emitted directly as self-contained modules.

Program (almide build --target wasm, as shipped)	structural leg
Hello, world	831 B

Measured on almide 0.66.0 (dev), 2026-10-01, from docs/benchmarks/wasm-size.txt; no post-hoc optimizer touches the shipped bytes (--wasm-opt is opt-in and its output is not the renderer's own module).

Rust on the same wasm target is 40 KB+ for Hello, world even fully size-tuned; the native minigit CLI binary is 418 KB stripped with 0 dependencies. The byte-by-byte dissection, measured 2026-07-23 (it also covers the incumbent leg, since retired by #2761): docs/wasm/WASM-OUTPUT.md.

Against handwritten Rust the arithmetic kernels sit at parity (n-body, spectral-norm 1.00×; the ratchet's anchored rows). Where Almide has information Rust does not — a tree whose whole lifetime is one check(make(depth)) expression, proven by the effect system — it is faster than the ordinary Rust for the same program:

Workload (bench.py, median of 9, interleaved)	optimization	Almide / ordinary Rust	without it (ALMIDE_REGION_OFF=1 / ALMIDE_FAN_SEQUENTIAL=1)	CI runner
binarytrees	region window (#1991)	0.35 (d17) / 0.32 (d19)	1.25	0.61
treealloc	region window (#1991)	0.30 (d20) / 0.30 (d21)	1.10	0.61 (est.)
fannkuchredux	parallel fan (#2044)	0.21 (n10) / 0.12 (n11)	1.06	0.60 (est.)

Two ratios per row are the two input sizes (the win holds at both); the Rust side is the ordinary program a person writes for it — a Box per node, one thread, no arena, no unsafe, no SIMD — compiled with the same rustc flags, and the "without it" column is the same Almide source with the region window turned off, so the whole gap is that one optimization. The absolute ratio is allocator-dependent (the CI runner frees a Box cheaper), the direction is not: the perf-ratchet job fails if either row reaches 1.0 or the ablation stops paying. Declaration and methodology: docs/project/BENCHMARKS.md. Ledger: docs/benchmarks/native-victory.txt (almide 0.62.0, 2026-09-08).

Measured on almide 0.59.1, arm64 Darwin, examples/lisp.almd (268 lines), 2026-08-27. Every row is an N-run MEAN — a single run of a 30ms process is scheduler noise. Cold clears BOTH $TMPDIR/almide-run and the dependency cache before each repetition; clearing only the latter measures a warm build. Regenerate with almide run tools/almide-gates/src/main.almd -- bench; the ratchet (-- bench --check) fails CI at 1.5x.

scenario	time	runs
almide check	15.2 ms	20
build, warm (content-cache hit)	237.2 ms	5
build, cold	635.3 ms	3
build, cold, --target wasm	61.7 ms	3

almide check scales linearly: over a 2k → 30k-line ladder of this repo's own stdlib the log-log slope of check time against project lines is 1.13 (1.0 is linear, 2.0 quadratic) and the 10k-line rung costs 4.4× the empty-project floor — measured 2026-08-13, held by scripts/check-edit-loop-scale.sh, table in BENCHMARKS.md. Native runtime against handwritten Rust: 1.00× on n-body and spectral-norm, 1.16–1.18× on fasta and FFT, ~1.6× where the workload is list materialization (#1004), CI-gated ratio ratchet (scoreboard). Wasm runtime, measured and gated (#1701):

Benchmark (almide bench, verify-then-time, min of 2×5 interleaved)	wasm/native, main only	cold start (spawn vs compile + instantiate)
nbody	1.10×	1.14×
spectralnorm	1.21×	1.22×
binarytrees	1.07×	1.06×
treealloc	1.04×	1.04×
fasta	1.52×	1.50×
fannkuchredux	9.41×	8.79×
mandelbrot	1.11×	1.10×
onebrc	1.26×	1.33×
fft	1.53×	1.53×
strchurn	0.85×	0.85×
listbuild_append	1.96×	1.95×
listbuild_combinator	1.88×	1.86×
listbuild_prealloc	1.68×	1.68×
mapbuild	0.67×	0.72×

Embedded wasm host (Perceus RC in linear memory) against the native binary, same machine, same run. The ratio times the program's own main, entry to return, on both legs (native in-process, wasm around the host call): process spawn and module compile/instantiate are outside it, and the cold-start column shows them (#2980). Small workloads run at a ledger-fixed size (args=) so main is long enough to time. Cross-engine ratios do NOT cancel hardware (a 2-core CI runner measures nbody ~10x worse), so the stamped ratio verdict runs on the stamping machine class; CI gates the STATUS taxonomy below and judges the wasm leg by a same-runner A/B against the latest release binary (interleaved, min-of-runs, ab_band in the ledger — #2143) (scripts/check-wasm-runtime-ratio.sh). binarytrees and mandelbrot run their fan arms on the embedded host's thread pool; fannkuchredux's fan runs sequentially on wasm, which is most of its gap. The unmeasured corpus cells stay honest instead of estimated: 0 wall on the wasm build path, 0 exhaust the embedded heap (#1729) — each re-measured every gate run, so a cell that starts benching fails the gate until its row is promoted. Ledger: docs/benchmarks/wasm-runtime.txt (almide 0.65.1 (dev), 2026-09-29).

How It Works

One frontend, one IR, one renderer per target:

flowchart LR
    SRC([".almd"]) --> FE["Lexer → Parser → Type Checker → Lowering"] --> IR(["IR"])
    IR --> NANO["Nanopass Pipeline<br/>semantic rewrites"] --> TMPL["Template Renderer<br/>TOML-driven"] --> RS([".rs → native binary"])
    IR --> STRUCT["structural leg<br/>commissioned engine, direct emit"] --> WASM([".wasm"])

Loading

Native. The Nanopass pipeline applies target-specific transformations — ResultPropagation (Rust ?), CloneInsertion (Rust borrow analysis), LICM (loop-invariant code motion). The Template Renderer is purely syntactic: every semantic decision is already encoded in the IR.

WebAssembly. The structural leg — the engine commissioned in #1599, almide::wasm_leg front + crates/almide-wasm emitter, entered through render_wasm_module_routed in src/cli/build.rs — is the only wasm renderer. It was accepted at 610/610 byte-identical to native on the wasm_cross corpus, and its build artifacts ship in the WASI form (#1588) so they run on stock runtimes. A program it does not lower is an honest error (error[E082], naming the wall and the function), never a fallback: the incumbent v1 leg that once took those shapes lost its last route in #2752 and was deleted in #2761. ALMIDE_VERIFIED_DEBUG=1 narrates the route.

almide run app.almd                  # Compile + execute (native)
almide build app.almd --target wasm  # Build WebAssembly (WASI)
almide test                          # Find and run all test blocks (recursive)
almide check app.almd                # Type check only
almide check app.almd --target wasm  # + the wasm build route: E081/E082 at check time (#1922)
almide fmt app.almd                  # Format source code

Run almide --help for the full command list (compile, add, deps, clean, …). Pipeline and module map: docs/ARCHITECTURE.md; the wasm leg in detail: docs/wasm/.

What's next — v1, the Trust Spine

The Perceus proof above proves one compiler pass, once. v1 generalizes that principle to the whole pipeline — instead of proving the 100k-line compiler, it proves a tiny checker and has the compiler emit a certificate on every build that the checker re-verifies. If the checker accepts, the artifact has the property — a theorem that never mentions the compiler's internals. That collapses the trusted base from ~100,000 lines to the extracted checker (~1,400 lines of OCaml, machine-derived from the proofs), and asks a harder question than testing ever can: not "do the tests pass?" but "can a machine prove the output is correct?" The architecture, the receipts (C-SAFE / C-REPRO / C-FAITHFUL / C-PROVEN), and why builds are slower on purpose: docs/TRUST-SPINE.md.

Project Status

Category	Status
Maturity	Pre-1.0, under active development on develop; the LLM-facing surface is frozen by STABILITY.md (declared 2026-08-20)
Support	Latest release line only, pre-1.0 — policy and versioning guarantees: SUPPORT.md · vulnerabilities: SECURITY.md
Compiler	Pure Rust, single binary, 0 ICE
Targets	Rust (native), WASM (direct emit — the structural leg, see How It Works)
Verified codegen	Structural wasm leg: byte-exact corpus and mutation gates, trusted with its per-build certificate pending (#2755–#2760); the PCC-certified incumbent leg (per-build re-verification since 0.29.0) was retired by #2761
Codegen	Rust: Nanopass + TOML templates; wasm: structural engine → direct emit (the v0 emitter and the incumbent MIR→WAT renderer are retired — a wall is an error, never a fallback)
Artifacts	.almdi module interface files via almide compile
Playground	Live — the compiler runs as WASM in the browser

Derived count	Value
Stdlib	1028 functions across 45 modules — self-hosted .almd, signature indexes regenerated from the compiler by tools/gen-stdlib-doc-index.py
Tests	475 .almd test files under spec/ (almide test spec/) + the 372-contract cross-target ledger

Mutation score — 41/41 mutants caught (100.0 %), 0 survived, 0 stale: the full release-shape net sweep of ci/mutations/ (scripts/check-mutation-gate.sh), stamped 2026-09-22 from mutation-sweep run 35650396971 at 3b02f7dc4.

Ecosystem and documentation

• almide-grammar — the single source of truth for syntax (keywords, operators, precedence, TextMate scopes), written in Almide; the compiler generates its lexer keyword table from it at build time, so compiler and tooling cannot drift
• vscode-almide · tree-sitter-almide (Neovim, Helix, Zed) · playground
• docs/CHEATSHEET.md — quick reference for AI code generation · docs/SPEC.md — the language specification · docs/GRAMMAR.md — EBNF grammar + stdlib reference
• docs/design/DESIGN.md — design philosophy · docs/design/EQUIVALENCE.md — the byte-identity claim · docs/design/MEMORY-SAFETY.md — the proven/trusted account · docs/TRUST-SPINE.md — v1
• docs/contracts/ — behavior-contract ledger · docs/stdlib/ — standard library, per module · docs/project/BENCHMARKS.md — sizes, runtime, edit-loop scale · docs/roadmap/ — evolution plans

Contributing

Issues and pull requests are welcome on GitHub. After cloning, install the git hooks (brew install lefthook && lefthook install); commits must be in English (enforced by the commit-msg hook). Project conventions: CLAUDE.md.

License

Licensed under either of MIT or Apache 2.0 at your option.