Bend Skill Guide

When using Bend:

• Run bend guide to learn the core syntax and concepts.
• Use LAWS.bend to declare business rules, invariants, and specifications.
• Use PROOF.bend to formally prove every law declared in LAWS.bend.
• Run bend check <file>.bend and bend PROOF.bend before committing.
• Parallelize operations whenever compute-intensive or recursive tree reductions are involved.

Rules

• Write laws for whatever should never break, and parallelize everything you want running fast.
• The Common Errors reference must be updated whenever new error patterns are identified.
• All files and documentation in this skill are maintained strictly in English.

Hello, World!

Bend's syntax is Python-shaped, with pure functional semantics closer to Haskell / Lean, while remaining resource-aware like Rust. A hello world is a typed definition returning an IO block:

import Base

def main() -> IO(Unit):
  do IO<Unit>:
    IO.print("Hello, world!")

To run it:

bend hello.bend

Bend is a pure language where side-effects are encapsulated inside the IO Monad.

Reference Summary & Examples

Core Language & Topics

• Tooling: CLI commands (bend, bend check, bend -c), compilation flags, and workflows.
• Syntax Reference: Complete grammar reference, literal formats, AST forms, and assignment rules.
• Types and Functions: Data types, constructors, function signatures, and affine annotations (+).
• Closures: Anonymous functions, lambda expressions, and environment capture.
• Recursion and Termination: Structural recursion, totality checks, and @unsafe escape hatch.
• Parallelism: Multi-threaded execution, parallel dispatch (a b = f(x) g(y)), and GPU execution (f!(x)).
• Arrays: Single-owner mutable arrays with $O(1)$ in-place updates (a[i] <- v).
• Quantities: Variable usage tracking with &0 (erased), &1 (affine), and &2 (unrestricted data).
• Kinds: Type classification into Data (copiable) and Type (linear/non-copiable).
• Templates: Compile-time monomorphization and metaprogramming via ~ arguments.
• Laws and Proofs: Formal verification workflow using LAWS.bend and PROOF.bend.
• IO and Concurrency: Encapsulating effects, file operations, sockets, and asynchronous tasks.
• Monads: Monadic computation chains, do blocks, Maybe, and Result.
• Apps: Interactive 2D/3D graphical applications and game engines in pure Bend.
• The Base Library: Standard prelude types (Bool, Nat, U32, F32, List) and core operations.
• Modules: Multi-file organization, relative imports, aliasing, and diamond deduplication.
• Common Errors: Comprehensive catalog of common compiler errors, anti-patterns, and idiomatic fixes.

Test Subskills (Located in .agents/skills/bend/tests/)

• Base Tests: Standard library primitives, algebraic types, and built-in type operations.
• Check Tests: Type checking, kind inference, and affine linearity verification.
• Compile Tests: Compiler pipeline, lowering targets, and native C/CUDA code generation.
• Comptime Tests: Compile-time evaluation, constant folding, and template macro expansion.
• Cost Tests: Work metrics, interaction net rewrite accounting, and complexity analysis.
• Eval Tests: Term reduction, normal-form computation, and operational evaluation.
• Flatten Tests: Pattern matching compilation and decision tree flattening.
• Gfx Tests: 2D/3D graphics rendering, pixel shaders, and display loops.
• Grade Tests: Resource grading, quantities (&0, &1, &2), and erased proof parameters.
• Halt Tests: Termination checking, structural recursion, and infinite loop prevention.
• Import Tests: Module resolution, relative paths, and cross-file proof linking.
• IO Tests: Side-effect encapsulation, concurrent TCP sockets, and file streams.
• Page Tests: Memory paging and single-owner mutable array operations.
• Parse Tests: Lexical analysis, syntax grammar rules, and operator precedence.
• Printer Tests: Pretty-printing, AST desugaring, and term formatting.
• Proof Tests: Theorem proving, propositional equality, reflexivity ({==}), and rewrites.
• Reg Tests: Backend register allocation and affine variable lifecycles.
• RFC Tests: Bend language specifications, modern idioms, and RFC evolutions.
• Run Tests: End-to-end execution on CPU and CUDA GPU backends.
• Show Tests: Interactive term inspection, hole diagnostics (?name), and goal debugging.
• Spec Tests: Formal operational semantics and core language invariants.
• State Tests: Pure state threading, state monads, and mutable cell abstractions.
• Stats Tests: Runtime profiling, node allocation metrics, and throughput counters.
• Stuck Tests: Stuck term diagnostics, reduction failures, and deadlock resolution.

Further Reading

• demos/: Complete example programs (HTTP server, ray tracer, parallel sorting, 3D boss fight game).
• bend2/base.bend: The official Base prelude library (or run bend base).
• paper/BendTT.pdf & paper/BendRT.pdf: Formal type theory and runtime specifications.