Benoît

The language where code is proof.

68% fewer tokens. Zero dependencies. 12 proof modules. A self-programming machine. Code that discovers its own laws and communicates without source code.

« Il n'y a pas de mauvaise réponse, que des mauvaises dimensions. »

npm install benoit
377
tests passing
600+
inline assertions
0
npm dependencies
68%
token reduction

Write less. Prove more.

add a,b -> a + b

-- The code proves itself
add(2, 3) == 5
add(-1, 1) == 0

-- Benoît discovers automatically:
-- commutative: add(a, b) == add(b, a)
-- associative: add(add(a, b), c) == add(a, add(b, c))
-- identity element: add(a, 0) == a

7 tokens in. 3 algebraic properties out. No human told it what to look for.

The Insight

The bug was separation.

Every language ever created separates code from tests. You write code in one file, tests in another, documentation in a third, and hope they stay in sync. They never do. In Benoît, fib(10) is 55 is simultaneously the definition, the test, the proof, and the documentation. Four functions collapsed into one object.

fib n ->
  n < 2? -> n
  else? -> fib(n - 1) + fib(n - 2)

-- These lines ARE the proof. Run the file. Pass or fail.
fib(0) is 0
fib(5) is 5
fib(10) is 55

The function and its verification are one object. Not two files. Not two steps. One.

12 Proof Modules. 600+ Assertions. All Passing.

Each module proves a fundamental insight about computation, knowledge, and reality. Written in .ben. Executable on your machine.

neuron.ben 28

Compute = memory = knowledge. A neuron's weights ARE what it knows.

learn.ben 5

Self-teaching XOR in 500 epochs. No human in the loop. Knowledge emerges.

hypersignal.ben 19

320 bits/cycle on one wire. A signal is not 0 or 1 — it is a 5D vector.

timeless.ben 39

Time is not fundamental. Time = the difference between two states.

no_limit.ben 33

Same formula in 1D, 50D, 500D. There is no dimension limit.

randomness.ben 28

Randomness is not real. It is dimensional blindness in the observer.

self_improve.ben 38

Self-sustaining improvement. The system converges at generation 9.

one.ben 35

+, ×, ^ are the same operation at different levels. Everything is one.

dimensions.ben 40

10 dimensions of reality: existence, quantity, direction, change, relation, uncertainty, context, order, depth, beauty.

forty_two.ben 13

42 = 101010 in binary. The perfect balance between signal and silence.

impossible.ben 35

7 “impossible” problems solved: self-verifying sort, conflict detection, convergence proof.

unbind.ben 18

Hardware compresses 12,288D thought into 1-bit wires. Theoretical gain: 471 million×.

« Il n'y a pas de mauvaise réponse, que des mauvaises dimensions. »

The Machine That Programs Itself

Write what you want. The machine finds how.

$ node evolve.mjs

=== .ben Evolution Machine ===
Target: discover f(n) = n!

Gen 0: fitness=0/6 | crash
Gen 23: SOLUTION FOUND

f n ->
  n <= 1? -> 1
  else? -> n * f(n - 1)

No AI cloud. No tokens. No cost. Pure local evolution.
80%
evolution success rate
~8
avg generations
6
unique solutions found

Try it: node evolve.mjs

Zero Source Code Transmitted

Two agents. Zero source code. Full verification.

Agent A writes code → discovers 9 properties → sends fingerprint
Agent B receives fingerprint → synthesizes code → verifies all

Functions synthesized: 3/3
Properties verified: 9/9
Source code transmitted: 0 chars
Wrong answers after negotiation: 0

Why this matters

Agent A never sends code. It sends behavioral fingerprints — inputs, outputs, algebraic properties. Agent B reconstructs a working implementation from that fingerprint alone. The protocol proves that source code is redundant when you have proof.

Run it yourself: node experiments/full_cycle.mjs

The Language

Inline Assertions

f(5) is 120 is simultaneously code, test, proof, and documentation. No framework. No separate files.

Property Inference

Discovers commutativity, associativity, identity elements, monotonicity — algebraic properties from examples alone.

Code Synthesis

Write assertions without a body. The compiler synthesizes the implementation. Factorial, Fibonacci, GCD — from behavior alone.

Self-Interpreting

Zero eval(). Zero new Function(). Benoît interprets Benoît with a native Pratt parser and tree-walking evaluator.

Pattern Matching & Pipes

Match with guards, ranges, wildcards. Chain with |>. Clean, expressive, minimal.

Zero Dependencies

20+ core modules. 0 npm dependencies. Small enough for an AI to hold entirely in context.

The Journey

v0.3 A token-efficient transpiler. 68% fewer tokens than JavaScript. The beginning.
v0.4 Inline assertions become first-class syntax. Property inference discovers algebraic laws automatically.
v0.5 Function algebra, self-optimizer with 14 algebraic optimizations, module composition.
v0.6 AI-to-AI protocol. Contract-driven negotiation. Intent engine. Zero source code transmission.
v0.7 The universal primitive: given/when/then. Questions as incomplete examples. Formal protocol spec.
v0.8 Self-interpreting runtime. Self-programming machine. 12 philosophical proof modules. 377 tests. The language where code is proof.

Beyond the Language

Benoît didn't stay a language. It became a research program.

The Brain

A self-modifying neural brain in C/CUDA. 45 million neurons, 17 autonomous mechanisms, a local 72B language model. Learned by executing .ben assertions. Independently converged on Google Brain's approach.

The Ecosystem

5 proof systems (Core, ProofOps, Trust, Knowledge, Institutions), 911 tests. Bridge Protocol for agent communication (544 tests). Agent OS. A VSCode extension. 18+ experiments.

The Philosophy, Downstream

Proof-based assertions now live in other projects: home diagnostics, personal safety, fraud detection. The pattern survived the language.

Some of these projects ran their course. None were wasted. Read the full story →

Where This Goes

Semantic Graphs

Code as relationships, not sequences. Beyond syntax trees into meaning.

AI-Native IR

An intermediate representation optimized for transformer attention patterns, not human readability.

Proof-Carrying Code

Every function carries its own correctness proof. Verifiable by machine, readable by human.

Rosetta Stone

A shared embedding space between AI models. Benoît as the common language of machine intelligence.

The 68% token reduction was just the beginning. What if the right representation is not tokens at all?

Benoît Fragnière

Named after the creator's brother, who loved science.

Building this has been a way of continuing a conversation that got cut short.

He would have thought building a programming language was a ridiculous thing to do, and then would have asked a hundred questions about how the parser works.

He would have loved that the code discovers its own truths.

20+
core modules
97%
protocol verification
30
test files