Show HN: Aver – AI가 작성하고 인간이 검토할 수 있도록 설계된 언어

Aver is a statically typed language designed for AI to write in and humans to review, with a fast interpreter for iteration, a bytecode VM for runtime execution, a Rust backend for deployment, Lean proof export for pure core logic, and Dafny verification for automated law checking via Z3. It 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: - effects are part of the function signature - decisions live next to the code they explain - pure behavior lives in colocated verify blocks - effectful behavior can be recorded and replayed deterministically aver context exports the contract-level view of a module graph for humans or LLMsaver compile turns an Aver module graph into a Rust/Cargo projectaver proof exports the pure subset of an Aver module graph to a Lean 4 proof project (default) or Dafny verification file (--backend dafny ) This 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. Read the Aver Manifesto for the longer argument, or Common Pushback for questions, objections, and honest answers. cargo install aver-lang Then try it with a tiny file: cat > hello.av String ? "Greets a user." "Hello, {name}" fn runCli() -> Unit ? "Starts the CLI." "Prints one rendered response." ! [Args.get, Console.print] Console.print("todo") verify greet greet("Aver") => "Hello, Aver" fn main() -> Unit ! [Console.print] Console.print(greet("Aver")) EOF aver run hello.av aver run hello.av --vm aver run hello.av --self-host aver verify hello.av aver verify hello.av --vm aver verify hello.av --json aver check hello.av aver check hello.av --json aver context hello.av aver compile hello.av -o out/ (cd out && cargo run) Unit is Aver's "no meaningful value" type, roughly like void and rendered as () in diagnostics. main often returns Unit , but it can also return Result ; aver run treats Result.Err(...) from main as a process failure. git clone https://github.com/jasisz/aver cd aver cargo install --path . --force aver run examples/core/calculator.av aver run examples/core/calculator.av --vm aver run examples/core/calculator.av --self-host aver verify examples/core/calculator.av aver verify examples/core/calculator.av --vm aver check examples/core/calculator.av aver context examples/core/calculator.av aver compile examples/core/calculator.av -o out/ (cd out && cargo run) aver proof examples/formal/law_auto.av -o proof/ (cd proof && lake build) aver run examples/services/console_demo.av --record recordings/ aver replay recordings/ --test --diff aver replay recordings/ --test --check-args aver replay recordings/ --test --json Requires: Rust stable toolchain. For editor integration: cargo install aver-lsp Then install the VS Code extension Aver.aver-lang , or configure your editor to start the aver-lsp binary directly. See editors/README.md for VS Code, Sublime Text, and manual LSP setup notes. module Payments intent = "Processes transactions with an explicit audit trail." exposes [charge] decision UseResultNotExceptions date = "2024-01-15" reason = "Invisible exceptions lose money at runtime." "Callers must handle failure — Result forces that at the call site." chosen = "Result" rejected = ["Exceptions", "Nullable"] impacts = [charge] fn charge(account: String, amount: Int) -> Result ? "Charges account. Returns txn ID or a human-readable error." match amount 0 -> Result.Err("Cannot charge zero") _ -> Result.Ok("txn-{account}-{amount}") verify charge charge("alice", 100) => Result.Ok("txn-alice-100") charge("bob", 0) => Result.Err("Cannot charge zero") No if /else . No loops. No exceptions. No nulls. No implicit side effects. Aver is intentionally opinionated. These omissions are part of the design, not missing features: - no if /else - branching goes throughmatch - no for /while - iteration is recursion or explicit list operations - no exceptions - failure is Result - no null - absence isOption - no closures - functions are top-level and explicit The point is to remove classes of implicit behavior that are easy for AI to generate and annoying for humans to audit. For the fuller language rationale, see docs/language.md. LLMs can produce function bodies quickly. They are much worse at preserving the information reviewers actually need: - what a function is allowed to do - why a design was chosen - what behavior must keep holding after a refactor - what a new human or model needs to understand the codebase without reading everything Traditional languages usually push that into comments, external docs, stale tests, or team memory. Aver makes those concerns part of the language and tooling. The intended workflow is explicit: AI writes Aver, humans review contracts and intent, and execution happens through the interpreter or bytecode VM during development, with deployment also available through Rust code generation. aver run hello.