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. (
foldover 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.