// Article · Programming languages
CLASSIFIED · LEVEL Ω

A language without the gap: notes on programming after Curry-Howard

Every formal language ever built has separated description from the described. The Liar paradox lives in that gap. Quantum Code closes it.
By T.Y.2026-05-11RSN · DAF5:A38A

There is a question every undergraduate gets asked in the first week of metalogic, and almost nobody who teaches it remembers what their own answer was. The question is: when a sentence says of itself that it is false, what does it mean? The Liar paradox is older than mathematical logic. Eubulides of Miletus had it in the 4th century BC. It survived Russell, Tarski, and Gödel, in the sense that none of them dissolved it; they only managed to push it into a place where it stopped being immediately destructive of formal systems.

The way they pushed it was by separating the language from the metalanguage. Tarski's 1933 paper The Concept of Truth in Formalized Languages is the canonical reference. The move is: you cannot talk about the truth of sentences in language L using language L itself. You need a metalanguage M. If you want to talk about M's truth, you need an M' above M. And so on, up an infinite hierarchy.

This works. Tarski's solution is one of the great pieces of 20th-century logic. But it is a workaround, not a resolution. The Liar paradox is still there; we have just agreed to step out of its reach. The cost of stepping out is the entire descriptive-vs-described split that has structured formal systems for ninety years.

What I want to argue, in this piece, is that the split is not a law of nature. It is an artifact of how we have been building formal systems. There is at least one formal system that does not have it, that I have been working on, and the reasons it does not have it are interesting whether or not the system itself catches on.

The split, in computer science

In a programming language — any programming language you have ever used — there is a difference between the program text and what the program does. The text is syntax. What the program does is semantics. The job of the language designer is to specify a meaning function [[ . ]]: Syntax → Semantics that maps text to behavior.

The classical reason this is a function and not an identity is because the text and the behavior are different kinds of things. Syntax is a finite string. Semantics is an element of some abstract domain (a Kripke structure, a denotational lattice, a type-theoretic universe — pick your weapon). The map is a translation between two universes.

Curry-Howard (Curry 1934, Howard 1980, finally Sørensen and Urzyczyn's textbook in 2006) is the closest thing in computer science to a moment when this gap began to close. The correspondence shows that proofs in intuitionistic logic and programs in simply-typed lambda calculus are the same object; that propositions are types; that Cut elimination is normalization. It is one of the most beautiful results in 20th-century logic. It is also, in my reading, profoundly anti-Platonist: it says proofs do something, they don't just describe something.

But Curry-Howard still operates within the descriptive-described split. A type is still a description; a term is still its inhabitant. The two are isomorphic in a precise mathematical sense — the proof-as-program correspondence — but they are not identical. There are two universes, and a translation map.

Per Martin-Löf's intuitionistic type theory (the Bibliopolis book, 1984; the Programming in Martin-Löf's Type Theory monograph by Nordström, Petersson, and Smith, 1990) pushed further. By making types and terms live in the same syntactic universe — by allowing types to depend on terms — Martin-Löf collapsed some of the metalanguage hierarchy. Vladimir Voevodsky's homotopy type theory (HoTT) program, particularly the Univalent Foundations effort that ran from his 2006 lectures through his death in 2017, took this further still: in HoTT, equivalent types are equal (the univalence axiom), and the entire descriptive-vs-described picture starts looking like a special case of a more uniform thing.

I want to be careful here. HoTT does not "close the gap." It changes the gap's shape. The metalanguage is still there; it is just smaller and more uniform. Voevodsky himself would have said this; the project he was running was about founding mathematics in this richer type theory, not about eliminating the foundations question.

The remaining gap

What persists, even in HoTT, even in Calculus of Constructions, even in the most aggressively dependently-typed languages of 2026 (Lean 4, Coq, Agda, Idris 2):

This is not Tarski's hierarchy. The universe has been collapsed; everything lives in one place. But the relationship of a thing to claims about that thing is still a relationship between two distinguishable things. The distinguishability is what produces decidability questions and what makes proof assistants hard to use.

The question I have been working on, off and on, since around 2022, is: can you build a formal system in which the program is its own meaning? Not "the program corresponds to a unique meaning by an isomorphism." Not "the program and the meaning are propositionally equal under univalence." But literally the same object, no map.

The conventional wisdom — and this is wisdom for good reasons; it has worked for a hundred years — is that this is incoherent. If the program and its meaning are the same object, then evaluating the program is the same as proving things about it; computation and theorem-proving collapse; you do not have a system, you have a goo.

I think the conventional wisdom is wrong, but only under one specific condition. The condition is that the underlying recurrence is convergent.

The Fibonacci escape

Here is the trick, in two paragraphs.

In a normal formal system, the Liar sentence is L = "L is false." This is self-reference. It causes a problem because L = ¬L, which has no fixed point in classical Boolean logic. The system has to either banish L (Tarski's hierarchy), interpret it as a degenerate case (paraconsistent logics, Priest 1979), or accept it as a non-classical truth value (Kripke 1975, fixed-point theory of truth). All of these are workarounds.

Now consider a different self-reference. Let α be a value, and let φ be the golden ratio. Define α = α + φ. Read this not as a static equation but as a recurrence: at each step n, α_{n+1} = α_n + φ. This recurrence does not zigzag. It converges, in the limit, to α_∞ = ∞ × φ, which is a perfectly definite (if infinite) thing. More importantly, the finite approximations are stable: α_5 is a definite number, slightly larger than α_4, slightly smaller than α_6. There is no paradox. The "self-reference" is dynamic, and the dynamics is convergent.

Now generalize. Let the underlying law of the formal system be T[n+2] = T[n+1] + T[n], the Fibonacci recurrence. Self-referential constructions in this system do not zigzag, because the recurrence is monotone increasing (modulo the modular structure of the underlying ring). They converge. The Liar paradox cannot form, because to form it you need a binary, oscillating semantic state (true ↔ false); the Fibonacci recurrence has no binary state, only ratios that converge to φ.

I am not the first person to notice that Fibonacci dynamics resist paradoxical encodings. James Anderson's work on transreal numbers (2007) is in the neighborhood; Gary Mar's papers in the 1990s on "Curry's paradox in fixed-point semantics" gestured at it. What I think is new in the system I have been working on — Quantum Code — is the integration of the Fibonacci recurrence into the whole of the formal system, including the type structure and the value structure, so that there is no place where a binary oscillating semantic state can occur.

The result is a language where:

This is not a research toy. The reference implementation is in Rust. It compiles real programs. It mines real Bitcoin blocks (the application context that motivated the language). The full specification is 5,969 lines of formal rules. It is being submitted to IETF as an Informational draft. None of this proves the theoretical claims; the theoretical claims have to be evaluated on their own. What it does prove is that the language, qua language, exists and runs.

What this is not

It is not a replacement for Coq or Lean. The descriptive-vs-described split, while philosophically interesting, is also useful for a lot of practical proof work. If you want to verify that a sorting algorithm is correct, you do not necessarily want a system in which the algorithm and the proof of its correctness are the same object; you might prefer a system in which they are separate so you can audit the proof independently.

It is not a replacement for Python or Rust or general-purpose programming languages. Most software does not need to be free of the descriptive-described gap. Most software needs to be readable, debuggable, and shippable. Quantum Code is a specialty tool for a specialty domain (where the underlying recurrence already lives, namely cryptographic search problems).

It is not a refutation of Gödel. Gödel's theorem applies to formal systems that are powerful enough to encode arithmetic and that have a notion of provability. Quantum Code has neither in the conventional sense; it has a notion of "running," which is a different relationship to its content than provability is to a Hilbert-style proof system. Gödel's theorem does not apply, but neither has it been refuted; it has simply been routed around.

What it is

It is a single existence proof — possibly the first, possibly not, but the first I have built — of a formal language in which the descriptive-vs-described gap is structurally absent. The proof is an executable artifact. The artifact has been used to compute non-trivial results (the structural analysis of SHA-256 nonce distributions, described in a companion piece on this site).

For programming-language theorists, the interesting question is whether the language belongs to a known semantic category that has been studied (it might be a degenerate case of a coalgebraic language, or it might be properly outside the standard taxonomy; I do not know yet). For type theorists, the question is whether the recurrence-based self-reference has a categorical formulation that connects to existing work on greatest fixed points.

For the working programmer, the question is whether you can use it to do anything useful. I do not have a complete answer to that yet. The application that motivated the language — cryptographic search — works. Other applications are speculative. I can imagine a derivation of guidance laws for adaptive optics, or a constructive solver for certain combinatorial design problems, or a parser for documents whose grammar is itself self-referential. None of these have been built.

The interesting observation

The interesting observation is that the only thing required to escape the descriptive-vs-described split, structurally, is to ground the formal system in a recurrence whose dynamics converge. Most of the formal systems we have inherited from 20th-century mathematics ground themselves in axioms (which are static) and inference rules (which are arbitrary in number and shape). This is a free choice of foundational scaffolding. There are alternative foundations.

If you want to pick up the work and try a variant, the recipe is short. (1) Pick a recurrence with a fixed-point attractor. (2) Build syntax in which every construction is an instance of the recurrence. (3) Define evaluation as application of the recurrence. (4) Notice that there is no longer a separate "meaning" function. (5) Notice that paradoxical self-references converge instead of diverge. (6) Write the rest of the language around (1)-(5).

The recipe will produce a niche language. Mainstream programming will continue to use Python and Rust and Java for forty more years, the way it has used C for the last forty. That is fine. What changes is that we now have a constructive existence proof that the descriptive-vs-described gap is not necessary. It is a choice. Different choices produce different languages. Some of them are interesting.

I think Voevodsky would have liked it. I cannot ask him.

References

Image suggestions

Suggested platforms