Bend is a programming language designed for the AI era, built on the premise that future code will be written by AI systems rather than humans. The core idea is to give AI a mathematically precise language to work with—one that's unambiguous enough to verify correctness without requiring humans to read every line. It targets three main goals: compile as fast as C on CPUs and CUDA on GPUs through strong types and linearity constraints, verify mathematical proofs faster than existing proof assistants (checking in seconds what takes other tools minutes), and run natively on both CPUs and GPUs without requiring manual thread management or kernel code. The language handles parallelization automatically by splitting work recursively across available cores. The standout feature is LAWS.bend, a file where you define mathematical rules your application must never break. When an AI edits your code, Bend's compiler demands a formal proof that these laws still hold. If the AI introduces a bug that violates a law—say, a feature that accidentally lets players win in a game where winning should be impossible—the compiler rejects the change and forces the AI to retry. This turns "make no mistakes" from a vague request into a machine-enforced guarantee. You simply ask your AI to write laws for critical invariants (like "the sum of all balances must be zero" in a financial system) and run the proof checker before committing code. The catch is that Bend is genuinely young and rough around the edges. It only supports three numeric types (Nat, U32, F32), has no standard libraries for JSON, HTTP, or regex, can't do incremental compilation, and runs slowly when compiling to native code. There's no debugger, formatter, or language server support. The compiler itself is 99% AI-written and hasn't been fully audited. Values are affine (can't be shared easily), recursion must terminate, and the whole thing works best on Linux or macOS for backend code. The language demands verbose, fully-annotated code with no type inference. It's a bet that the friction of these limitations is worth paying for the ability to mathematically verify AI-written code.