GitHub - ilyasergey/langlib: Esoteric Programming Languages, Formally

An open-source library of the semantics of esoteric and fun programming languages, written in Lean 4.

Esoteric languages are not meant for realistic software. They exist to make a point, to win a bet, to parody a committee, or simply to be difficult. Over the last fifty years they have accumulated into a large body of design knowledge: single-instruction machines, programs that are string-rewriting rules, programs laid out on a grid that wraps at every edge, programs that encrypt themselves as they run. This knowledge is scattered across personal pages, wikis, and long-dead FTP servers, and a good deal of it is folklore: claims repeated confidently and checked by nobody.

This project archives that knowledge in a form that cannot rot. Every language gets a written specification, an executable reference semantics, and machine-checked answers to the questions people actually argue about, starting with what each language can compute. On top of that sits a compiler from a language a human would willingly write in, whose correctness is proved rather than tested.

For each language, LangLib provides:

• a specification in docs/<langname>/, summarising the language's history, semantics, and quirks, with credits to its authors;
• a parser, a reference interpreter, and a standalone runner written in Lean, under Langlib/Languages/<Langname>/;
• examples you can run for fun, and a test suite, including differential tests against non-Lean reference implementations where available;
• a computational-class result: a claim that the language is or is not Turing complete, and a machine-checked proof of it;
• where the language can host one — Turing complete, or, like Malbolge, merely roomy enough — a compiler from Turpentine (.turp), the small readable imperative language that sits on top of the collection. It is named for the solvent: a Turing tarpit is a language where everything is possible and nothing is easy, and turpentine dissolves tar. Two compilation schemes are possible, one hand-written and one derived from the completeness proof, and the library keeps both.

Languages

Currently implemented (see docs/README.md for the full status matrix, including compilers):

• brainfuck (Urban Müller, 1993), eight one-character commands on a tape of bytes
• fractran (John Conway, 1987), whose programs are lists of fractions
• subleq (folklore OISC, de-facto conventions by Oleg Mazonka), one instruction: subtract, branch if the result is ≤ 0
• whitespace (Edwin Brady & Chris Morris, 2003), where only spaces, tabs and newlines are code
• ook (David Morgan-Mar, 2001), brainfuck for orangutans
• deadfish (Jonathan Todd Skinner, 2006), four commands, one accumulator, no loops
• befunge93 (Chris Pressey, 1993), a stack machine whose pointer roams a wrapping grid
• malbolge (Ben Olmstead, 1998), designed to be as hard to program as possible
• thue (John Colagioia, 2000), whose programs are string-rewriting rules
• piet (David Morgan-Mar, 2002), whose programs are abstract paintings
• brainloller (Lode Vandevenne, 2005), brainfuck encoded in pixels
• malbolge-unshackled (Ørjan Johansen, 2007), Malbolge with the memory bound taken out, which is what makes it Turing complete
• unlambda (David Madore, 1999), a functional language with no variables and no lambdas
• ski (Schönfinkel 1924, Curry 1930), not an esolang but the combinator calculus underneath Unlambda, and the other half of the library's functional route to universality
• Turpentine: the library's own human-readable front end, named for what dissolves a Turing tarpit

Current status

The two middle columns answer different questions. Turing-complete (TC) is the answer itself, as the literature or our own spec page gives it. TC claim mechanised is whether that answer is backed by a machine-checked theorem in this repository, and links it.

The last column names the Turpentine compilers a target has: each name links to that backend's compiler notes in docs/, and the parenthesis after it links the sources — the compiler itself, and its correctness proof where there is one. A derived one comes out of that language's completeness proof, so it is (certified) already, but it does not support I/O: it routes everything through a register machine, which has no way to read or write, so the program takes no input and leaves its result in answer. Its output is also enormous. A bespoke one is hand-written for that target: it emits compact, readable code and supports the whole language. (trusted) means tested rather than proved; (certified on a fragment) means a correctness theorem covers part of what the compiler accepts, and links it. Whitespace's says more than the others: on its fragment the compiled program performs the source's I/O events, in order, not merely its answer. Verified compilers below explains why the library keeps both kinds.

The two Malbolges have a bespoke compiler and no derived one, for opposite reasons. Malbolge Unshackled's completeness claim is still open, so there is no witness to derive a compiler from yet; its backend compiles every program whose control flow can be settled before the target runs — loops, arrays and arithmetic included — but not one that reads input, because reading needs cells that survive re-execution, which is the completeness work itself. Malbolge's derived compiler will never exist — the language is proved bounded, so there is no witness to be had — and its bespoke backend is accordingly bounded by the machine rather than by us: it accepts every input-free program whose output fits in the 59049 words, and refuses anything larger with the count of bytes by which it does not fit.

The full matrix, with per-stage columns and links to every theorem, is in docs/README.md.

What a language is

One definition carries the whole library: running a program, proving a compiler correct, and claiming a language is or is not Turing complete are all stated against it.

ProgLang L is what every language here supplies.

class ProgLang (L : Type) where
  Prog  : Type                              -- abstract syntax
  parse : String → Except String Prog
  run   : Prog → Input → Nat → RunResult    -- program, input, fuel

L is an empty tag type that names the language rather than being its program type, so Befunge93 and BoundedByteBefunge93 can be two languages with two different answers. Input and RunResult are the shared execution model: a byte stream with a read cursor, and the bytes a run emitted together with how it ended. The Nat is fuel, a step budget, which is what makes run a total function even of a program that never terminates — it returns outOfFuel instead of diverging.

LawfulProgLang L is the one law the library asks of that shape: a completed run is a fixed point of more fuel. It looks like bookkeeping and is anything but. Every correctness statement here concludes with "for some fuel bound the compiled program halts with the right answer", and against an interpreter free to treat fuel as an input channel — halt with the right answer exactly at fuels that encode the answer, and at no others — that sentence is satisfiable by a language whose programs compute nothing. halted_stable pins fuel to its budget role, which is why the correctness structures and TuringComplete require the class rather than merely benefit from it, and why the correct_stable corollaries can read every "some fuel works" as "every fuel from some point on works" — the form a runner that picks its own bound actually needs. Every language in the library carries the instance, proved by one induction over its interpreter in Langlib/Languages/<Lang>/Stability.lean (the bounded Befunge-93 core's proof lives next to that model instead).

ProgLang is a class, not bundled data, because there is only ever one way to run a given language. Both live in Langlib/Common/Compilation.lean alongside the compiler-correctness definitions, which need them.

Computability

Esoteric-language folklore is full of claims nobody has checked. Every language here gets a claim about its computational class and a machine-checked proof of it. Per-language status is in the status matrix, and every result is audited by scripts/axioms.lean, because a proof resting on sorry type-checks exactly like a real one.

The yardstick: the URM

An unlimited register machine (URM), as Shepherdson and Sturgis defined it: countably many registers holding natural numbers, and four instructions — zero a register, increment it, copy one register to another, and jump to an instruction when two registers hold the same value. That is enough to compute every computable function, and small enough that simulating it inside a toy language is a day's work rather than a career.

LangLib does not define it. It comes from cslib, Lean's library of computer-science formalisations, so the claims are phrased in a vocabulary other people already use: Instr and Program, the step relation Step, and HaltsWithResult, which says a program run on an input vector halts with a given number in register 0.

Our additions are an executable interpreter — step and run — which cslib's relational semantics deliberately is not, plus the lemmas (step_eq_some_iff_Step, steps_run, haltsWithResult_of_haltsIn) tying the two together, so differential tests can run a URM program while every theorem is still stated against cslib's relation.

The three claims

All three live in Langlib/Common/Computability.lean, shared infrastructure rather than per-language files, so a claim means the same thing for every language.

TuringComplete L is the positive claim, and it is a witness rather than a proposition: a compiler from URM programs into L, an encoding of the machine's input, a decoding of its answer, and a proof that a compiled program halts with the right answer whenever the machine does. Writing that term down is what "we proved it complete" means here — half of it, anyway. The other half is that the witness's compile is a plain def that #eval can run: a witness conjured with Classical.choice would type-check for a language that computes nothing, and the axiom audit would not object, since choice is in the allowed set. What rules that out is that a noncomputable compile must say noncomputable in the source, and the differential tests execute compiled programs, which no such witness survives. The docstring spells the convention out. computes_of_turingComplete translates it into cslib's own vocabulary: such an L computes every URM-computable partial function, wherever that function is defined. The witness also pays for itself, because a compiler from a register machine is exactly what a certified Turpentine backend needs (see below).

BoundedStorage L is the negative claim: a configuration type, a bound on it per program and input, an injection into {0, …, bound - 1}, and two laws saying the machine is deterministic and that halting depends only on the configuration. From those, halting_decidable follows once and for all — a run that has not halted within bound steps has repeated a configuration and never will. A language with this witness has no computable TuringComplete witness — a meta-theorem rather than a Lean corollary, and by a subtler argument than "its halting would be undecidable", since the one-directional simulates breaks that naive reduction; the docstring gives the honest route, through the recursion theorem.

BoundedRun L asks for the same laws only where the pigeonhole argument uses them: at configurations a run actually reaches. Every BoundedStorage gives one. It exists because a language can have a state type that is wide (an unbounded array, an output that grows, an input cursor whose range depends on the input) while its reachable states are few, which is exactly Malbolge's situation.

Befunge-93 shows why this is worth doing. It is usually called incomplete because of its 80 by 25 playfield, but the real argument is that the reference implementation gives it byte-sized cells, making it a pushdown automaton — a stack machine, strictly weaker than a Turing machine. Our cells hold unbounded integers, so the language we implement is complete. Same name, two languages, and nobody noticed until the claim had to be written down precisely enough to prove.

Verified compilers

A Turpentine program reaches a target two ways, and the library keeps both.

Bespoke compilers are hand-written per target. They produce compact output and accept as much of Turpentine as the target can host, and they are what lake exe turpentine compile --to <lang> runs today for nine languages: brainfuck, whitespace, subleq, ook, brainloller, piet, fractran, malbolge-unshackled and malbolge. The first six take the whole language; the last three are bounded by their targets rather than by our effort — FRACTRAN has no I/O at all, the two Malbolge backends emit straight-line code, so they take any program that does not read, and Malbolge's additionally only what fits its 59049 words. Two of the nine are verified, on a fragment each: subleq and whitespace. Verifying the rest is per-language proof work.

Derived via the URM, a compiler costs nothing to write. A TuringComplete witness already contains a verified compiler from a register machine, so composing it with one shared Turpentine-to-register-machine pass, Compile/URM.lean, gives a correct-by-construction compiler into any language proved complete. The composition is proved once for an arbitrary target, so a new language costs one line. The catch is that everything runs through a machine simulation: the output is enormous, and the fragment is I/O-free.

Two notions of correct

Answer preservation is not behaviour preservation, and the library says which one it has proved. CertifiedCompiler is the answer-only statement: the compiled program halts and prints something that decodes to the number the source computed. That is exactly right for the derived compilers, whose fragment has no I/O, and much too weak for a backend that compiles read and print. IOCertifiedCompiler is the behavioural one: a run's observable behaviour is a Trace of the bytes it consumed and emitted, in order, and the compiled program has to reproduce the source's trace under an encoding the compiler declares up front, as well as its answer. toCertified proves the second implies the first, so upgrading a backend loses none of what was already proved about it. One backend has reached the behavioural statement: bespokeWhitespaceIO is the first inhabitant of IOCertifiedCompiler, over the same fragment its answer-only theorem covers, with encodeTrace the identity — the compiled program does not re-encode the source's I/O, it performs it. The remaining candidates and what each one needs are tabulated in certified-compilation.md.

Both compilation schemes are inhabitants of the same CertifiedCompiler interface, which pays off where a target has both: agree proves that any two verified compilers for one target decode the same answer out of every program both accept. Subleq and whitespace have both, so for those two "the derived compiler is an oracle for the hand-written one" is a theorem rather than a testing practice. Five of the seven unverified backends have a derived counterpart, and for those the derived one remains the strongest available check; the two Malbolges are checked by tests alone, Unshackled because its completeness claim is open and Malbolge because there is no completeness to claim.

Choose explicitly. compile and exec each take --bespoke or --tc, refuse both at once, and name the scheme they used, so a build log says which compiler made the artifact.

Why the bespoke compilers stay

"We proved one, so throw the other away" is the obvious wrong conclusion.

Some programs cannot go through a register machine at all. A URM takes its input before it runs and yields one number when it halts, so nothing that interleaves reading and writing can be expressed however far the certified fragment is widened. cat.turp will never compile that way. That is a property of the model rather than a gap in the work.

The output is not comparable. Compiling answer := 3 to brainfuck through the register machine produces 64 kilobytes and runs in billions of steps, because arithmetic becomes unary counting on a byte tape. The bespoke brainfuck backend compiles real programs into something that finishes.

The fragment is still narrowing in. Initialisers, &&, ||, /, % and arrays have landed; subtraction has not, and turned out to be harder than planned (the obvious Nat-valued semantics bridges the wrong way). Meanwhile the bespoke compilers accept the whole language today.

A verified bespoke compiler needs a stronger theorem than the derived one has. The certified statement observes a single number on runs that halt, which is adequate only because that fragment has no I/O. A backend for the whole language has to preserve a byte stream, consume input, and say what happens when a program prints and then diverges. That is a larger obligation, not the same one at higher effort.

The pipeline, the diagrams and the theorem that makes the composition work are in certified-compilation.md; what correctness means here, including how assert compiles, is in verification.md; and each target's own decisions are in docs/<langname>/compiler.md.

Turpentine is deeply embedded in Lean and modelled on Velvet. The longer-term plan is to compile shallowly-embedded Velvet to Turpentine, and from there to any esolang here, by relational compilation.

Building

Install elan, then:

lake build          # build the libraries and runners
lake test           # run the test suite

Running programs

Each language ships a runner named after it. Programs read from stdin and write to stdout, so pipe or redirect input, and the result is printed to your terminal. One example per language, with what you should see:

Brainfuck says hello.

lake exe brainfuck Langlib/Examples/Brainfuck/hello.b

Output:

Brainfuck reverses a word, reading it from stdin.

echo -n stressed | lake exe brainfuck --eof zero Langlib/Examples/Brainfuck/rev.b

Output:

Erik Bosman's 505-byte brainfuck quine prints itself, so diff says nothing.

lake exe brainfuck Langlib/Examples/Brainfuck/quine.b | diff - Langlib/Examples/Brainfuck/quine.b

Whitespace says hello, using a program made entirely of spaces and tabs.

lake exe whitespace Langlib/Examples/Whitespace/hello.ws

Output:

Ook! says hello, because brainfuck was not quite unreadable enough.

lake exe ook Langlib/Examples/Ook/hello.ook

Output:

Deadfish prints the ASCII codes of a greeting, one number per line, since printing letters is beyond it.

lake exe deadfish Langlib/Examples/Deadfish/hello.df

Output:

Subleq counts down on a machine with exactly one instruction.

lake exe subleq Langlib/Examples/Subleq/countdown.sq

Output:

FRACTRAN runs Conway's PRIMEGAME, which prints the primes as exponents of two. It has no halting condition, so cap it with --fuel.

lake exe fractran --n 2 --out pow2 --fuel 2000000 Langlib/Examples/Fractran/primegame.ft

Output:

Piet says hi, using a program that is an abstract painting.

lake exe piet Langlib/Examples/Piet/hi.ppm

Output:

Brainloller runs a brainfuck program encoded as coloured pixels.

lake exe brainloller Langlib/Examples/Brainloller/hello.ppm

Output:

Malbolge prints the hello world that a search program found in 2000, because no human could write one. The capitalisation is not a typo.

lake exe malbolge Langlib/Examples/Malbolge/hello.mal

Output:

Malbolge Unshackled runs a program nobody wrote: compiled/primes.mu is what the bespoke backend emits for a Turpentine source, checked into the tree and run here on Unshackled's own interpreter.

lake exe malbolge-unshackled --fuel 100000 Langlib/Examples/MalbolgeUnshackled/compiled/primes.mu

Output:

2
3
5
7
11
13
17
19
23
29

Turpentine, the readable front end, computes an integer square root.

echo 17 | lake exe turpentine run Langlib/Examples/Turpentine/isqrt.turp

Output:

Turpentine prints the primes up to 20, using the same trial division you would write in any language.

echo 20 | lake exe turpentine run Langlib/Examples/Turpentine/primes.turp

Output:

Compiling Turpentine

Turpentine programs can be interpreted, compiled to an esolang, or compiled and run in one step. Both compilers are available for each target: --bespoke (hand-written, whole language, compact, unverified) and --tc (derived from the target's Turing-completeness proof, correct by construction, larger, and restricted to an I/O-free fragment). Passing neither uses the bespoke one; passing both is an error.

Interpret it.

echo 17 | lake exe turpentine run Langlib/Examples/Turpentine/isqrt.turp

Output:

Compile and run in one step, using the hand-written backend.

echo 17 | lake exe turpentine exec --via whitespace --bespoke Langlib/Examples/Turpentine/isqrt.turp

Output:

Emit the target program instead, and note that the message says which compiler produced it.

lake exe turpentine compile --to subleq --bespoke -o /tmp/isqrt.sq Langlib/Examples/Turpentine/isqrt.turp

Output:

turpentine: wrote 22615 bytes to /tmp/isqrt.sq [bespoke, hand-written and unverified]

That file is an ordinary subleq program, so run it with subleq's own runner.

echo 17 | lake exe subleq /tmp/isqrt.sq

Output:

One target's compiled program is a picture. The Piet backend lays the program out as corridors of colour wired together with white, and emits a PPM.

lake exe turpentine compile --to piet --bespoke -o /tmp/tri.ppm Langlib/Examples/Turpentine/suite/triangle.turp

Output:

turpentine: wrote 43779 bytes to /tmp/tri.ppm [bespoke, hand-written and unverified]

That is an 88 x 42 codel image, and it runs like any other Piet program.

lake exe piet /tmp/tri.ppm

Output:

The certified compiler needs a program in its fragment: no I/O, no subtraction, and the result left in a variable called answer. Arrays are in, since the dispatch-chain work landed. sumsq.turp is written that way, and sums the squares below 5.

lake exe turpentine exec --via whitespace --tc Langlib/Examples/Turpentine/sumsq.turp

Output:

Outside that fragment it says which construct is the problem rather than emitting something it cannot justify.

echo 17 | lake exe turpentine exec --via whitespace --tc Langlib/Examples/Turpentine/isqrt.turp

Output:

turpentine exec: the certified URM fragment needs a variable named 'answer' to hold the answer: a URM has no output, so register 0 at halt is all there is
turpentine: the certified compiler accepts only the I/O-free fragment
  (no input or output, no subtraction, and the result in a
  variable named 'answer'); arrays, division and modulo are
  supported, and the message above names what was rejected.
turpentine: retry with --bespoke to compile the whole language.
turpentine: nothing was run

Every mode, including emitting to stdout and what the two schemes cost, is in certified-compilation.md.

Every runner accepts --fuel N (step budget), --verbose (report how the run ended: halted, runtime error, or out of fuel), and --help. Exit codes: 0 halted, 1 runtime error, 2 out of fuel, 3 parse or usage error. Example programs state their own usage in a comment where the language permits one; each language's README under Langlib/Languages/ has the full example inventory.

Documentation

• docs/README.md: the status matrix, one row per language, with computational class and compiler status.
• docs/PLAN.md: the staged workplan.
• docs/certified-compilation.md: verified compilation via the URM, with dependency diagrams.
• docs/verification.md: what compiler correctness means here and how the proofs factor.
• docs/conformance.md: the conformance suite — twenty programs, one expected output each, run on every language that can host them, compiled and hand-written.
• docs/TESTING.md: the two test layers, and what to install to run the differential tests.
• docs/ROADMAP.md: candidate languages.
• docs/RELATED.md: other people's formalisations.
• docs/PROGRESS.md: dated log, newest first.
• Per language: docs/<langname>/spec.md and docs/<langname>/compiler.md.

Contributing

Contributions of new languages, examples, tests, and proofs are welcome. See CONTRIBUTING.md for how to add a language and what the library expects from a submission.

Miscellanea

A survey of related efforts is in docs/RELATED.md.

License

LangLib is distributed under the Apache 2.0 license (see LICENSE). The library only implements languages whose designs are in the public domain or otherwise freely implementable; all example programs are either original, in the public domain, or credited to their authors under permissive terms.