{
  "$type": "site.standard.document",
  "bskyPostRef": {
    "cid": "bafyreiakikelecvk3m3xf476rsnpxs5z7qf2y4pogyyipxpty5xjjaiezm",
    "uri": "at://did:plc:pi6woz4d47bkuws673w2il2r/app.bsky.feed.post/3mkpkuew3hf22"
  },
  "path": "/t/a-first-look-at-token-efficiency/13981#post_6",
  "publishedAt": "2026-04-30T10:45:30.000Z",
  "site": "https://discourse.haskell.org",
  "tags": [
    "github.com",
    "GitHub - jasisz/aver: Aver is a programming language for auditable..."
  ],
  "textContent": "Jappie:\n\n> if you’d start desining a language with an LLM as the primary user in mind\n\nThis exists actually. I haven’t tried it yet but the features are pretty interesting:\n\ngithub.com\n\n### GitHub - jasisz/aver: Aver is a programming language for auditable...\n\nAver is a programming language for auditable AI-written code\n\n# **Aver**\n\nAver is a statically typed language designed for AI to write in and humans to review, with a bytecode VM for runtime execution, a Rust backend for deployment, a WASM backend for browser and embedded targets, Lean proof export for pure logic and classified effectful laws, and Dafny verification for automated law checking via Z3.\n\nIt is built around one idea: the risky part of AI-written code is usually not syntax, it is missing intent. Aver makes that intent explicit and machine-readable:\n\n  * effects are part of the function signature\n\n  * decisions live next to the code they explain\n\n  * pure behavior lives in colocated `verify`blocks\n\n  * selected effectful behavior can be verified with explicit stubs and trace assertions\n\n  * effectful runs can be recorded and replayed deterministically\n\n  * `aver why` scores every function’s justification coverage: description, verify, decisions\n\n  * `aver audit` runs all three axes — static checks, verify execution, format compliance — as a single CI gate\n\n  * `aver context` exports the contract-level view of a module graph for humans or LLMs\n\n  * `aver compile` turns an Aver module graph into a Rust/Cargo project or a standalone WASM module\n\n  * `aver proof` exports the pure subset of an Aver module graph to a Lean 4 proof project (default) or Dafny verification file (`--backend dafny`)\n\n\n\n\nThis is not a language optimized for humans to type by hand all day. It is optimized for AI to generate code that humans can inspect, constrain, test, and ship.",
  "title": "A first look at token efficiency"
}