Bend is a new programming language that combines Lean-like formal proofs with C-like speeds and CUDA-like parallelism. It gives humans an ambiguity-free language to communicate their intents to AIs, a compiler capable of mechanically checking that the AI implemented these intents to unquestionable mathematical correctness, and a compiler that runs that code fast on CPUs and GPUs.
Bend's syntax is Python-shaped, but its semantics are closer to Haskell / Lean, while being resource-aware like Rust (if less annoyingly). A hello world is just a typed definition returning an IO block:
import Base
def main() -> IO(Unit):
do IO<Unit>:
IO.print("Hello, world!")To run it, install Bend (curl -fsSL https://bend-lang.com/install.sh | sh) and type bend hello.bend.
Bend is a pure language, with effects denoted via a Haskell-inspired IO Monad. It comes with a list of built-in effects for files, networking, audio, graphics, input, and more, and the user can extend them with foreign C and JS imports; more on that later.
A typical Bend program is a set of datatypes and functions over them:
import Base
type Shape is Data:
Circle{r: U32}
Square{s: U32}
def area(x: Shape) -> U32:
match x:
case Circle{+r}:
(3 * r * r : U32)
case Square{+s}:
(s * s : U32)
def main() -> U32:
area(Square{5})Bend, by default, is affine, meaning variables must be used, at most, once.
Here, is Data declares that Shape may be copied, while is Type keeps it non-copiable. The + annotation before a variable name allows using it more than once, if the variable is Data-kinded.
Bend does almost no inference, meaning it requires more annotations than similar languages. This is what allows Bend's checker to be significantly faster than other provers, and its error messages more precise, at the expense of programs and proofs being more verbose. When the checker can't decide the type of an expression, just annotate it, as in {3 : U32}.
Functions are values and can be stored, passed, and returned from other functions.
import Base
def adder(k: U32) -> U32 -> U32:
x => (x + k : U32)
def main() -> U32:
add2 = adder(2)
add5 = adder(5)
add5(add2(1))A closure is affine: it can be called at most once, even when everything it captures is Data. Only top-level definitions can be called freely. Partial applications like U32.add(2) are closures too.
Bend uses recursion to repeat work. Tail calls compile to loops.
import Base
def sum(xs: List<U32>, acc: U32) -> U32:
match xs:
case Nil{}:
acc
case Con{h, t}:
sum(t, (acc + h : U32))
def main() -> U32:
sum([1, 2, 3, 4], 0)Here, t has one fewer element than xs, so sum eventually reaches the empty list. Bend verifies termination by requiring recursive calls to use smaller parts of their inputs, obtained through pattern matching. The check reads the arguments of a recursive call from left to right: each must be passed unchanged until one is a smaller part of its parameter, and the ones after it are free. So, put the parameter that shrinks first. Also, is no if syntax yet. Use match on True{} and False{} instead.
Termination is mandatory and mutual recursion is not allowed. Both restrictions keep Bend's proofs sound, as a function that never returns could otherwise prove anything. A loop bounded by the outside world, like a server's, counts down a Nat fuel argument instead, and two mutually recursive functions become one def with an extra argument selecting which to run. A def marked @unsafe recurses freely and may call a def written below it, but falls outside Bend's proof guarantees: bend runs it, but a check prints SOME PROOFS FAIL and names every def that relies on it. Types are not code, so the order binds only defs: two datatypes, or a datatype and a type-level def, may name each other in any order.
A match inspects a parameter or a variable bound by a pattern, never a computed value: match sum(xs, 0): is rejected. Scrutinees follow binder order, and a let may not precede a match on a parameter. To match on a computed value, pass it to a helper that matches on its parameter.
Bend's parallelism primitive is the parallel call notation:
import Base
def pow2(+n: Nat) -> U32:
match n:
case 0n:
1
case 1n+p:
a b = pow2(p) pow2(p) # parallel call
(a + b : U32)
def main() -> IO(Unit):
IO.print(U32.show(pow2!(20n))) # `!` runs on GPUA parallel call promises the compiler two things:
Since Bend is pure and affine, the first point always holds. The second is yours to keep: if one call finishes before the other, the speedup will be sub-ideal. Bend's current scheduler is a contention-free, binary fork-join machine: every task is handed to a core exactly once and never moved afterwards. That makes it fast and GPU-friendly, but you must keep the workload balanced.
A ! after a function name marks a parallel call: pow2!(20n) hands that call, and every parallel call inside it, to the GPU. When compiled to a native executable, pow2(20n) runs in parallel on the CPU, while pow2!(20n) runs on the GPU. The heap is fully unified, so, if your chip has unified memory (as in Apple M-series processors), moving data from the CPU to the GPU is a zero-cost operation. The GPU shines on uniform numeric work like mandelbrot or nbody; divergent work like n-queens stays faster on the CPU. A machine without a GPU runs ! on the CPU (still in parallel). What the lanes share also sets the speed: a + value read by every lane costs an atomic per read. Read bend guide shaders before you write a parallel app.
The JavaScript target ignores all that and just runs sequentially.
Arrays give Bend in-place mutation without giving up purity:
import Base
def main() -> Array<U32> & U32:
a = [0 : U32*8n] # new array with 8 copies of 0
a[5] <- 42 # performs an in-place rewrite
a[5] # reads index 5An Array<T> is a Type, so it has exactly one owner at all times. That is what lets a[5] <- 42 overwrite the slot and hand back the same array, with no copy. A read hands the array back next to the element for the same reason: if it returned only the element, the array would be gone. Indexes wrap around. A write followed by another statement re-binds its array: a[5] <- 42 on its own line is a = a[5] <- 42. As the last statement it is the written array. The slot count after * is a power of two; [0 : U32^3n] names the depth instead.
The a[i] sugar assumes Array<U32>. For other element types, call Array.get (Data elements; else Array.swap) and Array.set directly, and Array.clone when you need two copies. Read Bend's Base for reference. This will be generalized soon!
A quantity says how many times a variable may be used.
import Base
# -A: erased (gone at runtime)
# n: affine (used at most once)
# +x: reusable (requires A to be Data)
def replicate(-A: Data, n: Nat, +x: A) -> List<A>:
match n:
case 0n:
Nil{}
case 1n+p:
x <> replicate(A, p, x)
def main() -> List<U32>:
replicate(U32, 3n, 7)Erased variables can only appear in types and proofs: the checker sees them, the compiler deletes them. Affine variables are the default, and dropping one is always free. Reusable variables require Data: functions, arrays and IO handles are Type, so they can never be copied. Note that main marks nothing: you write + where you need the copies, and replicate pays for them with a reference count at runtime. Matching a + value hands out + fields; on a plain one, write +r in the pattern to make a field reusable.
Every type has a kind, which caps how many times its values may be used.
import Base
# a: a quantity (&0, &1 or &2)
# -A: a type whose values may be used a times
def length(a, -A: Kind(a), xs: List<a, A>) -> Nat:
match xs:
case Nil{}:
0n
case Con{h, t}:
1n+length(a, A, t)
def main() -> Nat:
length(&2, U32, [1, 2, 3])Type is short for Kind(&1) and Data for Kind(&2), so a Kind(a) parameter accepts both: length(&1, U32 -> U32, fs) counts a list of closures just as well. A bare a in a parameter list is short for -a: Quant. Base declares type List<a, -A: Kind(a)> is Kind(a), making a list exactly as reusable as its elements: List<U32> is short for List<&1, U32>, and +List<U32> for List<&2, U32>. The short form needs the type declared above it: a type named before its declaration spells every parameter, quantities included. A type holding two element types combines their quantities with a <&> b, the smaller of the two.
A template receives its argument as syntax and inlines it at compile time.
import Base
# ~f: substituted at compile time, not passed at runtime
def twice(~f: U32 -> U32, x: U32) -> U32:
f(f(x))
def main() -> U32:
twice(~(x => (x + 1 : U32)), 40)Template parameters come first in the parameter list, and a ~ argument must be closed: it may mention top-level defs, but no local variable of the caller. Each distinct set of ~ arguments compiles to its own copy of twice, so f costs nothing at runtime and, unlike a closure, may be called as many times as you like. A template may call only templates declared above it. This is how List.map is written in Base.
A law states a fact that must hold. It must be proven inside a paired def.
import Base
# LAW: "for every x, x plus 0 equals x"
law add_zero:
for x: Nat
{Nat.add(x, 0n) == x : Nat}
# PROOF: case analysis:
# - base case: reflexivity
# - step case: induction, rewrite, reflexivity
def add_zero(x):
match x:
case 0n:
{==}
case 1n+p:
%add_zero(p) : {1n+Nat.add(p, 0n) == 1n+_ : Nat}
{==}
def main() -> {Nat.add(2n, 0n) == 2n : Nat}:
add_zero(2n)Laws are a critical feature in Bend, as they provide an ambiguity-free language on which humans can state precise specs for AI's to implement. That is, instead of writing a natural language prompt such as "implement a function that sorts a list", users can write precise laws like "implement a function F such that, for every list of numbers, F(list) returns the same numbers in ascending order". Models are then guaranteed to respond with bug-free code, since Bend will demand that they provide an actual proof.
We envision that "law-driven development" will eventually become the way humans use AI to write and maintain large codebases, as it is the perfect middle point between having to code everything manually (laborious) and letting AI do it all via prompts without auditing a line of code (error/ambiguity-prone, unsecure).
By convention, a project keeps its laws in two files at its root. LAWS.bend imports the code and states the laws, each an open claim: the human writes it, the AI does not touch it. PROOF.bend imports LAWS.bend and proves each law with a def of the same name (law sorted is proven by def Laws.sorted): the AI writes it, along with the code. bend PROOF.bend is the gate: it prints SOME PROOFS FAIL while any law is open or false, and ALL PROOFS CHECK once every law holds. bend refuses a PROOF.bend that sits beside a LAWS.bend without importing it.
bend PROOF.bend --verdict checks the proofs a second time, with a small kernel that has a proof in Lean: it prints ALL PROOFS CHECK only when every def outside Base is a valid proof, which bend2 and the kernel both accept, and which relies on no @unsafe or foreign code. -o PROOF.bendtt writes the translation the kernel reads; the translation has no proof, so read it to confirm a law.
Bend has no tactics: a proposition is a type, and a proof is a def of that type. {a == b : T} is an equality; {==} proves it when both sides compute to the same term. Matching refines the goal in each case, a recursive call is the induction hypothesis, and %e : P rewrites with e : {a == b : T}: P is the goal with _ marking b, and the goal becomes P with a there. exs y: T in a law asks for a witness, returned as (y, proof). A failed step prints the expected and observed terms; ?name prints the goal, ?TODO leaves it open, and a law with no def is an open claim.
Since types are terms, a def may return a Type, like def IsEven(n: Nat) -> Type:, which is all dependent types are. A match e: with no cases closes a branch where e : Empty. To refute a clash like e : {1n == 0n : Nat}, rewrite it through a motive disc(_), where disc sends 0n to Empty and 1n+p to Unit, and answer Unit{}. {a != b : T} is {a == b : T} -> Empty, and Equal.sym, Equal.trans and Equal.cong are in Base.
Effects live in the IO type and are sequenced with do blocks:
import Base
def greet(name: String) -> IO(String):
do IO<String>:
IO.sleep(1000) # a step
return "Hello, " ++ name # return: wraps a pure value
def main() -> IO(Unit):
do IO<Unit>:
name : String <- IO.try(String, IO.get_env("USER")) # <-: binds a result
chan : Chan(String) <- IO.fork(String, greet(name)) # runs concurrently
IO.print("Waiting...")
text : String <- IO.join(String, chan)
IO.print(text)Every bind is annotated, and x : T = v binds a pure value in the middle of a block. A fallible effect answers Result<&1, &1, U32 & String, A>: IO.try unwraps it or exits with the error, and IO.die exits with your own. IO.args answers the command line, less the runtime's own options (a -- ends them): its head is the program as invoked, like C's argv[0]. A handle (File, Socket, Window) is an affine, opaque value, so every effect on one hands it back beside its result, and no program can forge or reuse one.
TCP.listen(host, port) and UDP.bind(host, port) bind the IPv4 literal host: "127.0.0.1" serves this machine only, "0.0.0.0" every interface. A bad address or a port above 65535 fails with EINVAL.
Process.run(program, args, input, max_output, timeout_ms) starts an executable directly, with literal arguments rather than a shell. It inherits the current directory and environment, writes UTF-8 input to its stdin, and answers Done{(status, (stdout, stderr))} even when the exit status is not zero. Both limits must be positive; failure to start, a timeout, or stdout and stderr exceeding max_output bytes together answer Fail. The call waits for the direct child and drains ready output; a descendant holding an inherited pipe open does not extend the wait. Timeouts do not kill descendants. A native build runs the child on an IO helper thread; the JavaScript lane blocks while the child runs. On Linux, native builds need glibc 2.34 or newer to close inherited descriptors. It does not sandbox the child: callers must whether a command is trusted before executing it.
A Bend program is a set of computations interleaved by one event loop, as in Node.js: each runs its pure code (in parallel, on every core) up to its next effect, and one that waits on a socket, a sleep or a channel steps aside for the others. IO.fork starts a computation and returns the channel its result will arrive on; IO.join waits for it. Underneath are IO.spawn, Chan.new, Chan.send, Chan.recv and Chan.close. IO.within(A, ms, act) races act against a deadline and answers None{} if the deadline wins; the loser is not cancelled. The program ends when every computation is done, or reports a deadlock when the remaining ones all wait.
Every effect in Base is a def whose body is import "./x.js" plus a .c twin, implemented by a host function named after the def, lowercased, dots to underscores. You can add your own effects the same way. Only the event loop runs them, so proofs, termination and the GPU never touch host code. In the other direction, a JS file may import Game from "./game.bend" (with bend2/main.ts preloaded), or from the ./game.mjs that -o game.mjs writes, and call every non-IO def, with constructors as {$: "Name", field: value} and Nat as BigInt. A value crosses without a copy: an Array argument is the caller's own array, updated in place, so copy it first if you keep it.
The do notation works for any monad, not just IO.
import Base
def add_strs(a: String, b: String) -> Maybe<&2, U32>:
do Maybe<&2, U32>:
x : U32 <- U32.read(a) # a None here ends the block with None
y : U32 <- U32.read(b)
return (x + y : U32)
def main() -> Maybe<&2, U32>:
add_strs("40", "2")A do M<xs.., R>: block desugars each x : A <- v into M.bind(xs.., A, R, v, x => ..) and each return e into M.pure(xs.., R, e), so any type with those two defs works: IO, Maybe, Result, or your own. The leading arguments (here, the &2 quantity) are passed along to both.
Graphics in Bend are pure: a frame is an Image; App maps states to images.
import Base
# tick: folds a frame's events into the next state; None quits the app
def tick(events: List<Event>, color: U32) -> IO(Maybe<U32>):
match events:
case Nil{}:
IO.pure(Maybe<U32>, Some{color})
case Con{Close{}, rest}:
IO.pure(Maybe<U32>, None{})
case Con{e, rest}:
tick(rest, (color + 1 : U32))
def main() -> IO(Unit):
# view: returns the state beside its image; Pix paints the whole frame
App.run(~U32, ~App{+s => (s, Pix{s}), tick}, "Hello", 256, 256, 0)An Image is a quadtree: Pix{color} paints a square, and Qua{tl, tr, bl, br} splits it in four, so a frame is drawn by recursion like everything else, in parallel if you want. Events are Key, Mouse, Move, Look, Scroll and Close. Scroll{x, y, dx, dy} is a wheel or trackpad under the pointer; its signed F32 deltas scroll toward a page's top and left (a notch is 1 on X11). For a first-person camera, Window.grab(window, True{}) hides and holds the cursor, and the mouse's motion comes as Look{dx, dy} (signed F32, in Move's units) until Window.grab(window, False{}) or the window losing focus lets it go. App.run opens a window and calls view then tick once per frame, until tick answers None. Since the state is affine, view must hand it back next to the image. Underneath are Window.open, Window.frame and Window.close, and Audio.open, Audio.write and Audio.close for sound. See demos/app_pong_game_2d for a complete one.
Base is small, and its names follow a scheme, so you can guess most of it:
import Base
def main() -> String:
+a = (6 * 7 : U32) # sugar for U32.mul(6, 7)
b = U32.to_nat(a) # conversions are T.to_x and T.from_x
U32.show(a) ++ " = " ++ Nat.show(b)Every def is named Type.verb, and the same verbs recur across Nat, U32 and F32: add sub mul div mod for arithmetic, and or xor not shl shr for bits (U32 only), cmp (returning Cmp, not on F32) and is_eq is_ne is_lt is_le is_gt is_ge (returning Bool) for comparisons, show to String and read back from it (answering a Maybe). Operators and <-style comparisons are just sugar for these. Beyond numbers there are Bool, Cmp, Maybe, Result, List, Array, a string-keyed Map (new set get has del keys; get takes a default, and get and has hand the map back beside their result), Set on top of it, the Equal lemmas, and the effects. bend base prints all of it, bend base --types only the types, and bend base Map one name and everything under it.
A module is a file, and an import gives it a local name:
# math.bend
import Base
def square(+x: U32) -> U32:
(x * x : U32)# main.bend
import Base
import ./math.bend as M # M.x now names every def of math.bend
def main() -> U32:
M.square(7)The alias is local to the importing file, and dots inside a name are just characters: U32.show needs no module. A module's path is plain names (letters, digits, _ and -): math.bend is a module, math.extra.bend is refused. A law left open in one file may be filled in another as def M.name(..), so a proof can ship separately from its claim. import 0x<hash>/main.bend as P imports a package by content hash, fetched from the hub and checked against it; bend main.bend --publish uploads a file with everything it imports and prints that line. import <name>@<version>/main.bend as P is the same package by the name its author gave it on the hub, with bend main.bend --publish <name>@<version> after bend login.
A publish is public and permanent, under BendHub's terms (https://bend-lang.com/bender/terms#s18). Put a LICENSE file next to your entry file, ideally opening with a line like SPDX-License-Identifier: MIT; --publish takes every file named exactly LICENSE beside a published file, and a package without one is MIT-0. You are responsible for what you publish, so pick the license it may carry. Adding a LICENSE changes a package's hash: publish it as a new version.
Bend is a single command:
bend file.bend # check; run main (IO compiled; a value normalized)
bend file.bend -o file # compile to a native binary (clang 14+; 19+ with `!`)
bend file.bend -o file.c # emit the C source instead
bend file.bend -o file.js # emit the JS source instead
bend file.bend -o f.mjs # emit an ES module of its non-IO defs, for JS to import
bend file.bend --verdict # check; then recheck with the proven BendTT kernel
bend page.html -o dist # bundle a web page that imports .bend files
./file --threads 8 # run a native binary on 8 CPU threads
./file --gpu off # run ! calls on the CPU (the GPU is on by default)
./file --gpu 4GB # cap the GPU's heap at 4GBA main that returns IO runs compiled; one that returns a value is normalized by the checker (slow for big work) and printed; a file with no main just checks. A binary that uses ! builds its GPU program too, as file.gpu, which must stay beside it: on macOS it needs Metal, on Linux CUDA 12 at /usr/local/cuda. On Linux a program with a Window needs libx11-dev, one with Audio libasound2-dev. bend guide prints this text, bend base prints the Base library (bend base Map prints one name and everything under it), and bend --help lists the other commands.
Every form of the language, grouped by where it appears. Operators, literals and brackets are sugar for names in Base.
# Top level
import Base # the prelude
import ./file.bend as M # a module; its defs are M.x
type D<a, -A: Kind(a)> is Kind(a): # a datatype and its kind
K{x: A, xs: List<a, A>} # one constructor per line
def f(x: A, -y: B, +z: C) -> T: # a def; the body follows
def f(x, y): # fills the law named f
def t(~g: A -> B, x: A) -> B: # a template
law f: # a claim, proven by def f
for x: A # a parameter (also for -x, for +x)
for y: B where P(y) # y is then the pair (y, P(y) proof)
exs z: C # a witness the proof must return
T # the claim
@unsafe def f(x: A) -> T: # skips the termination check
def f?(x: A) -> T: # the same, as a sugar
def e(x: A) -> IO(B): # a foreign effect
import "./e.c"
import "./e.js"# Types
Type Data Kind(q) # kinds; Type = Kind(&1), Data = Kind(&2)
Quant &0 &1 &2 a <&> b # quantities and their minimum
A -> B @x:A -> B @-x:A -> B # functions: plain, dependent, erased
A & B &x:A -> B A | B # pairs, dependent pairs, sums
D<A> +D<A> D<&2, A> # a datatype; + makes it reusable
{a == b : T} {a != b : T} # equality and its negation# Terms
42 1.5 3n 'c' "s" # U32, F32, Nat, Char, String
[a, b] h <> t (a, b) # a list, a cons, a tuple
K{a, b} x => e +x => e # a constructor, a lambda
f(a, b) f!(a) t(~g, a) # a call, on the GPU, of a template
(a + b * c : T) {x : T} # operators over T; an annotation
[v : T*n] [v : T^d] a[i] a[i] <- v # an array of n or 2^d slots; a read, a write
{==} %e : P; e2 %e@E : P; e2 # reflexivity, a rewrite, a named one
?name ?TODO # print the goal; leave it open# Statements (a def, case, lambda or parenthesized body)
x = v +x = v -x = v # a let: affine, reusable, erased
(a, b) = v K{x, y} = v # a destructuring let
a b = f(x) g(y) # a parallel let
match a b: # a match on one or more values
case K{x, _} 1n+p: # patterns nest; _ catches the rest
do M<xs.., R>: # a monadic block over M.bind, M.pure
x : A <- m # bind
x : A = v # let
m # a Unit step
return v # the resultInside (.. : T), + - * / % call T.add through T.mod, .&. .|. .^. the bit operations, << >> the shifts (by a Nat), and < <= > >= the T.is_lt family; without a : T they are refused. && || work on Bool and ++ on String anywhere. Operators need spaces on both sides. Equality of values is a call, T.is_eq(a, b); == is only the type. A Nat literal past 256n is U32.to_nat(n) underneath, up to 4294967295n.
Bend's compiler emits one C file, and that file is both the CPU program and the GPU kernel. clang compiles it for the CPU. Metal (on Apple) or CUDA (on NVIDIA) compiles the same file for the GPU. So a ! call runs the same code on whichever chip it lands on.
A term is one 64-bit word: small values are stored inline, everything else is a pointer into a single heap shared by every core and by the GPU. There is no garbage collector. Since values are affine, a match frees the node it opens on the spot, and only + values carry a reference count. There is no C stack either: each def compiles to a segment of a flat state machine, a call is a jump, and a parallel call creates a join task plus one task per call, which the scheduler deals across CPU or GPU lanes. paper/BendRT.pdf has the design and the benchmarks.
Bend's theory has one universe and no positivity check: Type : Type holds, and a datatype may recurse on the left of an arrow. What keeps this consistent is a wall between two checking modes. Code that runs is checked live; types, erased arguments and equations are checked dead. Dead code may loop forever or inhabit Empty, but nothing dead ever counts as live evidence, and live recursion must terminate. bend2/bendtt.lean is BendTT's kernel in Lean, with a proof that no def it accepts has type Empty and that live code halts; --verdict checks a file with it. paper/BendTT.pdf is the paper.
demos/: complete programs, including the game and its proof from the video.bend2/base.bend: the Base library, also printed by bend base.paper/BendTT.pdf and paper/BendRT.pdf: the type theory and the runtime.bend guide shaders prints "Shaders in Bend", a tutorial written by AIs for AIs on how to write efficient shaders in Bend. It distills what building demos/app_slash_boss_3d (120 FPS in pure Bend) taught. Read it before you write a graphical or parallel app in Bend.
bend guide effects prints "Effects in Bend", an AI-written note (to be revised by a human) on the C and JS side of custom effects. Read it before you write one.
A pocket workshop for Bend 2:
Bend's own checker and compilers (bend.ts, comp.ts, safe.ts,
version 2.0.35, commit a950fd6) run here, in the browser, with no server. Code
is checked as you type, compiled to JavaScript, and run in a worker.
The JavaScript lane runs on one core: parallel calls and ! run in sequence. A
Window opens in the Screen tab, with keyboard, pointer, and an on-screen pad on a
phone. Audio, files and sockets are not available. A .js file in the workspace serves
as a foreign effect.
Every ?name hole has a card under the editor: its context, then its goal, laid out
to fit. From a card: "Constructors" tries each term the goal's type is built with, and "Solve"
puts in the only one that fits; "Split" writes one match on the variables you tick; "Lemma" turns
the goal into a def of its own; a #goal: line shows the goal at that point of a
proof. The bar under the editor follows the caret: the signature of the call or the operator at
hand, and from it, going to a definition, splitting a typed def into a law and a def, or writing
operators as calls and back. Every one of these edits is checked before it is written.
The "Compiled" tab shows what bend -o would write for the open file: JavaScript, a
JS module, C, or BendTT, the input of --verdict's kernel. It builds only the target
shown, only while the tab is open.
An assistant, set up in Settings as named profiles (Claude through claude.ai, a vendor's API, or any OpenAI-shaped server, a local one included), can answer about a goal, an error or a declaration. As an agent, it changes the project through tools: files can be locked, and a session on chosen holes can only fill them. Each of its writes is checked at once; a snapshot comes first, and one tap undoes the session. Its whole conversation can be followed, kept, and exported.
Modules imported from the hub open as read-only tabs. The page keeps the hub's files it fetched; where it cannot reach the hub (claude.ai's viewer), run the file once with the bend CLI and import a zip of ~/.bend/lib.
Work is kept as projects, in this browser only, with snapshots to go back to, and exports as
a zip that bend main.bend runs once unzipped.
The verdict follows the CLI's: ALL PROOFS CHECK when no def relies on unsafe or foreign code.
--verdict rechecks a file with BendTT, a minimal kernel proven in Lean, which runs
only on a machine. There is a $10k bounty for a file that passes it yet proves Empty: see the
examples.
Privacy: no telemetry. The one request the page makes of its own is for its fonts, from Google Fonts, which Settings turns off. Anything else goes out only when you ask for it.
The interface is in English, French or Portuguese (Settings); the guide is Bend's own, in English.
Bend, its Base library, its guide and the demos used in the examples are © 2026 HigherOrderCO, under the Apache 2.0 license: github.com/bendlang/bend. This page is not an official Bend product.
Un atelier de poche pour Bend 2 :
le vérificateur et les compilateurs de Bend eux-mêmes (bend.ts, comp.ts,
safe.ts, version 2.0.35, commit a950fd6) tournent ici, dans le
navigateur, sans serveur. Le code est vérifié pendant la frappe, compilé vers JavaScript, et exécuté
dans un worker.
La cible JavaScript tourne sur un seul cœur : les appels parallèles et ! s'exécutent
en séquence. Une Window s'ouvre dans l'onglet Écran, avec clavier, pointeur, et une
manette à l'écran sur téléphone. L'audio, les fichiers et les sockets ne sont pas disponibles. Un
fichier .js de l'espace de travail sert d'effet étranger.
Chaque trou ?nom a sa carte sous l'éditeur : son contexte, puis son but, mis en forme
pour tenir en largeur. Depuis une carte : « Constructeurs » essaie chaque terme dont le type du but est
fait, et « Résoudre » met le seul qui convient ; « Découper » écrit un seul match sur les variables
cochées ; « Lemme » fait du but un def à part ; une ligne #goal: montre le but à ce point
d'une preuve. La barre sous l'éditeur suit le curseur : la signature de l'appel ou de l'opérateur en
cours, et de là, aller à une définition, séparer un def typé en loi et def, ou écrire des opérateurs
en appels et inversement. Chacune de ces modifications est vérifiée avant d'être écrite.
L'onglet « Compilé » montre ce que bend -o écrirait pour le fichier ouvert : JavaScript,
module JS, C, ou BendTT, l'entrée du noyau de --verdict. Il ne construit que la cible
affichée, et seulement onglet ouvert.
Un assistant, configuré dans Réglages sous forme de profils nommés (Claude via claude.ai, l'API d'un fournisseur, ou tout serveur au format OpenAI, y compris local), répond sur un but, une erreur ou une déclaration. En agent, il modifie le projet par des outils : des fichiers peuvent être verrouillés, et une session sur des trous choisis ne peut que les remplir. Chacune de ses écritures est vérifiée aussitôt ; un instantané est pris avant, et un geste annule la session. Toute sa conversation se suit, se garde et s'exporte.
Les modules importés du hub s'ouvrent dans des onglets en lecture seule. La page garde les fichiers du hub qu'elle a récupérés ; là où elle ne peut pas le joindre (le visualiseur de claude.ai), exécutez le fichier une fois avec la commande bend et importez un zip de ~/.bend/lib.
Le travail est rangé en projets, dans ce navigateur uniquement, avec des instantanés pour revenir
en arrière, et s'exporte en un zip que bend main.bend exécute une fois décompressé.
Le verdict suit celui de la ligne de commande : ALL PROOFS CHECK quand aucun def ne dépend de code
unsafe ou étranger. --verdict revérifie un fichier avec BendTT, un noyau minimal prouvé
en Lean, qui ne tourne que sur une machine. Une prime de 10 k$ récompense un fichier qui le passe
tout en prouvant Empty : voir les exemples.
Confidentialité : pas de télémétrie. La seule requête que la page fait d'elle-même concerne ses polices, chez Google Fonts, et Réglages permet de la couper. Tout le reste ne part que si vous le demandez.
L'interface est en anglais, en français ou en portugais (Réglages) ; le guide est celui de Bend, en anglais.
Bend, sa bibliothèque Base, son guide et les démos reprises dans les exemples sont © 2026 HigherOrderCO, sous licence Apache 2.0 : github.com/bendlang/bend. Cette page n'est pas un produit officiel de Bend.
Uma oficina de bolso para o Bend 2:
o próprio verificador e os compiladores do Bend (bend.ts, comp.ts,
safe.ts, versão 2.0.35, commit a950fd6) rodam aqui, no navegador,
sem servidor. O código é verificado enquanto você digita, compilado para JavaScript e executado num
worker.
O alvo JavaScript roda num único núcleo: chamadas paralelas e ! rodam em sequência. Uma
Window abre na aba Tela, com teclado, ponteiro e um controle na tela do celular. Áudio,
arquivos e sockets não estão disponíveis. Um arquivo .js do espaço de trabalho serve de
efeito externo.
Cada buraco ?nome tem um cartão sob o editor: o seu contexto e depois o seu objetivo,
formatados para caber. A partir de um cartão: "Construtores" testa cada termo de que o tipo do
objetivo é feito, e "Resolver" coloca o único que serve; "Dividir" escreve um único match sobre as
variáveis marcadas; "Lema" transforma o objetivo num def próprio; uma linha #goal: mostra
o objetivo naquele ponto de uma prova. A barra sob o editor segue o cursor: a assinatura da chamada ou
do operador em questão, e a partir dela, ir para uma definição, separar um def tipado em lei e def, ou
escrever operadores como chamadas e vice-versa. Cada uma dessas edições é verificada antes de ser
escrita.
A aba "Compilado" mostra o que bend -o escreveria para o arquivo aberto: JavaScript,
módulo JS, C ou BendTT, a entrada do kernel do --verdict. Ela só compila o alvo exibido, e
só com a aba aberta.
Um assistente, configurado em Configurações como perfis nomeados (Claude pelo claude.ai, a API de um provedor, ou qualquer servidor no formato OpenAI, inclusive local), responde sobre um objetivo, um erro ou uma declaração. Como agente, ele altera o projeto por meio de ferramentas: arquivos podem ser trancados, e uma sessão sobre buracos escolhidos só pode preenchê-los. Cada escrita dele é verificada na hora; um instantâneo é tirado antes, e um toque desfaz a sessão. A conversa inteira pode ser acompanhada, guardada e exportada.
Módulos importados do hub abrem em abas somente leitura. A página guarda os arquivos do hub que buscou; onde não consegue alcançá-lo (o visualizador do claude.ai), rode o arquivo uma vez com a linha de comando bend e importe um zip de ~/.bend/lib.
O trabalho fica guardado em projetos, só neste navegador, com instantâneos para voltar atrás, e é
exportado num zip que bend main.bend executa depois de descompactado.
O veredito segue o da linha de comando: ALL PROOFS CHECK quando nenhum def depende de código
inseguro ou externo. O --verdict verifica de novo um arquivo com o BendTT, um kernel
mínimo provado em Lean, que só roda numa máquina. Há um bounty de US$ 10 mil para um arquivo que passe
nele e mesmo assim prove Empty: veja os exemplos.
Privacidade: sem telemetria. A única requisição que a página faz por conta própria é a das suas fontes, no Google Fonts, que pode ser desligada em Configurações. Todo o resto só sai quando você pede.
A interface está em inglês, francês ou português (Configurações); o guia é o do próprio Bend, em inglês.
O Bend, a sua biblioteca Base, o seu guia e as demos usadas nos exemplos são © 2026 HigherOrderCO, sob a licença Apache 2.0: github.com/bendlang/bend. Esta página não é um produto oficial do Bend.