the 60 s video: bend-ml.mp4
bend-ml is machine learning for Bend 2. The shape of every tensor lives in its type, so a product of mismatched matrices does not compile, and the structural guarantees (a tokenizer that never loses a byte, a reverse mode that agrees with the forward mode) are laws that Bend's kernel checks. Five packages are on BendHub, and two demos run on them, an MNIST classifier and GPT-2 small, both checked against PyTorch.
# (2x3) · (4x5): does not compile
def bad() -> TA.MMul<2n, 3n, 5n>:
TA.Mat.matmul(2n, 3n, 5n, 0n, TA.Mat.zeros(2n, 3n), TA.Mat.zeros(4n, 5n))The same holds for every layer of a training step: the gradient of a weight matrix must have the shape of Xᵀ·dY, and a reshape only compiles with a proof that the number of elements does not change.
the reshape case
| Package | Version | What it is | Proved LAWS |
|---|---|---|---|
bend-ml-nat-lemmas |
0.1.1.0 | Nat and List lemmas that Base does not have |
add_comm, add_assoc, mul_comm, mul_assoc, mul_dist, append_assoc, length_append, product_append... (15) |
bend-ml-bpe-tokenizer |
0.1.2.0 | Byte-level BPE tokenizer (GPT-2 style) | roundtrip decode(encode(s)) = s, vocab_bound, dec_append, train_wf, roundtrip_trained |
bend-ml-tensor |
0.1.2.0 | Vec<n> and Mat<r,c> with the shape in the type, over lists |
reshape_swap, reshape_flat |
bend-ml-tensor-array |
0.1.3.0 | the same guarantees over a flat Array<F32>, ~50x faster |
cap_ok; typed matmul, matmul_nt, matmul_tn |
bend-ml-autograd |
0.1.1.0 | Automatic differentiation and layers with typed backward | reverse_eq_forward |
import bend-ml-tensor-array@0.1.3.0/main.bend as TA
import bend-ml-bpe-tokenizer@0.1.2.0/main.bend as BPEEvery package passes bend X/main.bend --verdict, the re-check by Bend's Lean-proved kernel, with no @unsafe and no ?TODO. Numbers are a different matter: F32 is not a real number, so the numerics are tested against PyTorch, NumPy and tiktoken instead of proved. docs/AUDIT.md lists the trust base.
| Demo | Result |
|---|---|
| MNIST, 784-128-10 MLP | about 7 s per epoch (v1: 544 s). Loss and hits identical to PyTorch with the same weights and batches: 0.5204771 / 9129, then 0.27043572 / 9298, then 0.2156194 / 9418. |
| GPT-2 small, 124 M | about 0.1 s per token (v1: 3 s). The same tokens as PyTorch on 11 prompts, logits within 2e-4; the tokenizer matches tiktoken on 79 texts. Loading takes ~7 s and ~1.5 GB. |
why PyTorch is still ahead
Bend 2.0.35 generates scalar code, with no BLAS or SIMD: on the same matrix product PyTorch does 62 G multiply-adds/s on one thread and Bend with an Array ~2.3 G/s. Parallelism adds ~2 to 4x on this hybrid CPU. The GPU (a user-local CUDA 12 makes ! run on the RTX 4050, see docs/gpu-setup.md) is 3.8x faster on compute-bound flat loops but 3 to 18x slower on our memory-bound kernels, so the benchmarks use the CPU. Full tables: MNIST, GPT-2, and NOTES.md, experiments 1 to 10.
- Types can carry the shapes of a whole training step, and they cost nothing at run time: the dimensions are erased.
- Proofs cover the structure, tests cover the numbers. Of the 24 laws, the ones that matter most are the tokenizer roundtrip,
reverse_eq_forward, the reshape size and the array capacity. - The trust base is small and written down: the kernel, Base's
F32primitives, and the fact thatArray.new(d)gives2^dslots. - Speed is bounded by the compiler, not by the types. Flat arrays gave ~49x, parallel blocks ~2x; what is left is BLAS and SIMD.
- Copying is the hidden cost: splitting a matrix for parallel work by copying it costs more than the arithmetic of a matrix · vector.
- The GPU only helps compute-bound work; our kernels are chains of dependent pointer loads.
- Measuring corrected some of my early claims: PyTorch takes 21 ms per token, not 150 ms; the GPU is not "slower everywhere"; and the "~10 GB" of GPT-2 memory was virtual size (the resident peak is ~1.5 GB).
Linux x86_64 (or WSL), clang ≥ 14, Python ≥ 3.12, curl, ~3 GB of disk, 8 GB of RAM for the GPT-2 check.
git clone https://github.com/nuxyel/bend-ml.git && cd bend-ml
make setup # Bend 2.0.35 (SHA256-checked), Lean 4.34.0, Python venv, data; no sudo
make check # 31 checks, about 1.5 min
make check-full # 36 checks with GPT-2 and MNIST, about 5 min
make media # regenerate the figures and the video on this pagemake setup-lite skips the 550 MB GPT-2 download. CI runs make check-full on every push. The history was rewritten on 2026-10-04 (English messages, smaller commits), so clone again if you have an older copy.
limits
- PyTorch is faster (see 04).
- The GPT-2 weights become trees of nodes; loading streams 1 MB blocks into the arrays, with a ~1.5 GB resident peak (the process reserves ~10 GB of address space).
- Only
Nat,U32andF32; noF64. Mat<r,c>does not carry "capacity ≥ r·c" in its type: the constructors establish it with the provedcap_ok, and thatArray.new(d)gives2^dslots is trusted.- The GPT-2 pre-tokenizer classifies code points up to U+1FFFF with a table generated from Unicode; above that, and for invalid UTF-8, everything counts as a letter.
structure
nat-lemmas/ bpe/ tensor/ tensor-array/ autograd/ packages (main.bend, README, LICENSE)
demos/mnist demos/gpt2 demos with README and BENCHMARK
reference/ PyTorch, tiktoken and check_all.py
poc/ bench/ proofs of concept and micro-benchmarks
docs/ audit guide, launch material, media
NOTES.md decisions, findings and debts
MIT · the visual identity uses Bend's own colours, from bend-lang.com