Skip to content

Latest commit

 

History

10,965 Commits

Folders and files

NameName
Last commit message
Last commit date
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

Almide

The language where LLM edits survive.

CI License: MIT / Apache-2.0 Ask DeepWiki

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.96+ (the almide package's rust-version, because the binary embeds the wasmtime host; CI builds with 1.96.0): 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() } runs each arm on its own thread natively and one after another on wasm; fan.map / fan.any / fan.settle return results in list order on both, fan.map runs every element and surfaces the lowest-index Err (dialect epoch 7), and natively it runs on threads only for a pure callback over scalars (an effect callback runs one element at a time). Every native arm and element writes into its own output timeline, flushed in list order, so what concurrent arms print comes out in source order on both targets, and a trap waits for the elements below it (ADR-0024 steps 1 and 3, C-004, C-005, C-200).
  • 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 with almide 0.29.0 (it has not been re-run on a later compiler), 100% pass, the most concise of 5 languages (233 LOC), and a faster agent wall-clock than Gleam and MoonBit but slower than Rust and TypeScript (573 s against 297 s) — 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. Output printed from concurrent fan { } arms is inside the guarantee: each native arm writes into its own timeline, flushed in source order, so it reads as it does on wasm (C-004, ADR-0024 step 1).

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, 100 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 VM, no GC, no interpreter — native compiles through Rust to machine code, and WASM is emitted directly as self-contained modules (the runtime support a program reaches is linked in and the rest is pruned).

Program (almide build --target wasm, as shipped) develop released v0.66.0
Hello, world 325 B 953 B

The develop column is the develop build at 5f39c06ba, after the v0.66.0 release (almide --version: almide 0.66.0 (dev, 5f39c06ba)), measured 2026-10-03; CI rebuilds it on every push and fails if the bytes move without a restamp of docs/benchmarks/wasm-size.txt. The released column is the compiler from the v0.66.0 release asset (almide 0.66.0 (release, 819bbc74f), gh release download v0.66.0 -R almide/almide), measured 2026-10-03. 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: 40,379 B with rustc 1.96.1, wasm32-wasip1, opt-level="z", lto, strip, panic="abort", codegen-units=1 (64,844 B with the default release profile), measured 2026-10-03 by the recipe at the bottom of WASM-OUTPUT.md. The native CLI-shaped benchmark (research/benchmark/perf/native/cli_app.almd, built by research/benchmark/perf/native/measure.sh) is 464,488 B stripped on macOS arm64 with no crate dependencies (only libSystem is linked), measured 2026-10-03 with both the develop build and the v0.66.0 release. 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 and spectral-norm 1.00× on an Apple M4 Pro (2026-07-30), and 1.065× and 1.032× on the ubuntu-latest CI runner (develop CI run 37092258733, 2026-10-03). 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, M4 Pro without it (ALMIDE_REGION_OFF=1 / ALMIDE_FAN_SEQUENTIAL=1), M4 Pro ubuntu-latest CI runner
binarytrees region window (#1991) 0.35 (d17) / 0.32 (d19) 1.25 0.581 (d17)
treealloc region window (#1991) 0.30 (d20) / 0.30 (d21) 1.10 0.365 (d20)
fannkuchredux parallel fan (#2044) 0.21 (n10) / 0.12 (n11) 1.06 0.315 (n11)

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. The M4 Pro columns were measured on almide 0.62.0, 2026-09-08 and have not been re-measured since; the runner column is what the perf-ratchet job of develop CI run 37092258733 printed at 466cac59b (a develop build carrying version 0.66.0, not the 0.66.0 release), 2026-10-03 (the size is in each cell).

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 close to 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, on an Apple M4 Pro (2026-07-30, FFT re-measured 2026-08-13): 1.00× on n-body and spectral-norm, 1.16× on fasta, 1.18× on FFT (scoreboard). The listbuild rows read 1.47–1.69× there and 0.87–1.05× on the CI runner (2026-10-03); their gap on the M4 Pro is the deterministic software sin/cos that byte-identity needs, not list building (measured 2026-08-13, scripts/perf-ratio-baseline.txt). The ubuntu-latest runner re-measures every row on each develop CI run, and the perf-ratchet job fails an anchored row (n-body, spectral-norm, fasta, FFT, wordfreq) that drifts more than 40% past its committed baseline (run 37092258733, 2026-10-03: fasta 0.757×, FFT 1.002×). 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 1.28× 1.28×
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). Of these rows only fannkuchredux runs its fan in parallel: native on threads (#2044), the embedded wasm host on separate instances of the module (#3003, ADR-0011 §D2a; every other wasm host runs it sequentially, byte-identical); binarytrees' and mandelbrot's fan.map callbacks run sequentially on both legs (user time equals wall time on both, measured 2026-10-03). 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 (a develop build carrying version 0.65.1, not the 0.65.1 release, 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 whole 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 the whole compiler (about 300,000 lines of Rust under src/ and crates/, test directories excluded, counted 2026-10-03) 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
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 1029 functions across 45 modules — self-hosted .almd, signature indexes regenerated from the compiler by tools/gen-stdlib-doc-index.py
Tests 486 .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

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.

About

A statically-typed programming language optimized for LLM code generation. Compiles to Rust and WebAssembly.

Topics

Resources

Security policy

Stars

34 stars

Watchers

0 watching

Forks

Releases

Packages

Contributors

Languages