weft-lang 0.2.0

Weft — the Thread's native code format: content-addressed, verified, total program graphs that cannot diverge, allocate unboundedly, or lie about what they are.
Documentation

Weft — the Thread's native code format (reference implementation)

Ship intent, not instructions. A Weft program is a typed, total, effect-explicit term graph, identified by the hash of its canonical encoding. What crosses the wire is the same object that gets verified; execution backends (this crate's reference interpreter first) compile or interpret it locally. Spec: docs/spec/weft-v0.1.md.

v0.1 scope — deliberately austere:

  • First-order and non-recursive. Definitions call other definitions by content hash; since a definition's hash doesn't exist until it is built, cycles are unconstructible and every program terminates by construction. (fold over finite data arrives in v0.2.)
  • No local names. Variables are de Bruijn indices, so alpha-equivalent programs are identical programs — same bytes, same hash. Names live outside the code, as metadata.
  • Deterministic core: integers, booleans, text. Division by zero is defined (= 0), so no arithmetic traps exist. No floats.
  • Effects are values. Constructing an [Action] performs nothing; the host (the browser) receives the returned actions and decides. A definition's declared effect row must cover everything it (and its callees, transitively) can construct — the row IS the permission.
  • Cost is static. The verifier computes a fuel bound per definition; the interpreter meters actual fuel. Verified code cannot run away.