Ik heb de RealWorld-app gebouwd in Lean 4

1. Introductie

Lean 4 is een functionele programmeertaal uit dezelfde familie als Haskell en OCaml. De meeste mensen kennen het als een proof assistant (bewijsassistent). Onlangs heeft de standaardbibliotheek ook een HTTP-server gekregen. De community schrijft inmiddels ook de overige bibliotheken die gewone apps nodig hebben, zoals Postgres-drivers, cryptografie en HTML-rendering.

Maar kun je nu al een echte webapp bouwen in Lean? Om dit uit te zoeken heb ik RealWorld gebouwd. RealWorld is een bekende referentie-app, een kloon van Medium die wordt geleverd met officiële testsuites voor zowel de API als de website. Mijn versie is volledig geschreven in Lean, inclusief het frontend-gedeelte, waarbij datastar-lean wordt gebruikt voor interactiviteit. De code staat op GitHub.

Ik heb dit bericht geschreven als een wiskundig paper, mede omdat dit leuk is en omdat het de structuur helder houdt. Het grootste deel van wat volgt is gewone engineering, zoals je dat in elke taal zou doen. De weinige zaken die daadwerkelijk bewezen zijn, zijn gemarkeerd als proposities. Lean controleert deze bewijzen elke keer dat de code wordt gebouwd.

2. Bestaan

De eerste vraag is of een RealWorld-app überhaupt in Lean gebouwd kan worden. De testsuites maken dit controleerbaar.

Definitie 1. Een RealWorld-implementatie is een programma dat voldoet aan de API-suite en de website-suite van RealWorld.

Theorem 1. Er bestaat een RealWorld-implementatie in Lean.

Het bewijs hiervoor is het bouwen van een dergelijke app. De testsuites definiëren wat er moet gebeuren. De API-tests sturen HTTP-verzoeken en controleren de terugkerende JSON, dus we hebben een server nodig. De data in die antwoorden moet tussen verzoeken bewaard blijven, wat betekent dat er een database nodig is. De website-tests klikken door de site in een echte browser, dus de server moet ook pagina's renderen.

Constructie 1: De server

De standaardbibliotheek van Lean heeft sinds april een HTTP-server, Std.Http, die alle low-level verbindingen afhandelt. Bovenop deze server gebruik ik lean-routing om de routes van de API in een tabel te declareren. Elke route heeft een pad met getypeerde parameters en een eigen handler. (Lees ← in de onderstaande code als await):

route_table Api
[ ...
comment := "/api/articles/:slug:String/comments/:id:Nat",
... ]

def deleteComment (env : Env) (slug : String) (id : Nat) : Handler := fun req => respond do
  Service.deleteComment env (← requireUser env req) slug id
  noContent

def routes (env : Env) : List (Route Result) :=
[ ...
.delete patterns.comment (deleteComment env),
... ]

Deze handler verwijdert een reactie. Hij controleert het login-token van de gebruiker met requireUser, roept de servicelaag aan om de reactie te verwijderen en antwoordt met 204 No Content. De website maakt gebruik van dezelfde servicelaag en volgt daarom exact dezelfde regels. De rest komt uit bibliotheken:

  • lean-json voor JSON
  • lean-libcrypto voor het hashen van wachtwoorden met OpenSSL's scrypt
  • lean-jose voor de login-tokens (JSON Web Tokens)
  • lean-middleware voor CORS, cookies en statische bestanden

Constructie 2: De database

De data bevindt zich in Postgres. Ik communiceer hiermee via leanpostgres, wat de C-client van Postgres wrapt en een pool van verbindingen bijhoudt. De SQL wordt direct in de code geschreven. Elke rij die terugkomt wordt omgezet in een Lean-structuur:

def userByEmail (db : Conn) (email : String) : IO (Option UserRow) := do
  first (← db sql!"SELECT id, username, email, password_hash, bio, image FROM users
                  WHERE email = {email}")

De {email} binnen sql! wordt een query-parameter, die Postgres apart van de SQL-tekst ontvangt. Hierdoor kan gebruikersinput nooit als SQL worden uitgevoerd. Het databaseschema is gewone SQL die door leanmigrate wordt toegepast wanneer de server start.

Constructie 3: De website

De pagina's worden op de server gerenderd met lean-html. Er zijn geen templates, omdat de HTML is geschreven als gewone Lean-functies. Deze functie toont een reactie, inclusief een prullenbak-icoon als jij de auteur bent:

def commentCard (viewer : Option Db.UserRow) (slug : String) (c : Db.CommentRow) : Node .flow :=
  let delete : List (Node .phrasing) :=
    if viewer.any (·.id == c.authorId) then
      [ span [ i [] { class_ := "ion-trash-a" } ] { class_ := "mod-options" }
        [onClick (action "delete" (Site.links.comment slug c.id.toInt.toNat))] ]
    else []
  div [
    div [ p [ c.body ] { class_ := "card-text" } ] { class_ := "card-block" },
    ...
  ] { class_ := "card", id := s!"comment-{c.id}" }

Die onClick is alle frontend-code die nodig is om een reactie te verwijderen. Datastar, een klein script op de pagina, stuurt het DELETE-verzoek wanneer op het icoon wordt geklikt en werkt vervolgens de pagina bij met het antwoord van de server. De server bouwt dat antwoord met dezelfde functie die de JSON-API gebruikt. Er is geen frontend-buildstap nodig omdat de pagina's simpelweg HTML zijn met één script. Op de server gebruik ik datastar-lean, de officiële Lean SDK voor Datastar.

Bewijs van Theorem 1. Voeg de drie onderdelen samen en draai beide testsuites tegen het resultaat. Ze slagen. ∎

Opmerking 1 (Over kosten). De Lean-backend bestaat uit 1.033 regels, de kortste van de vier implementaties waarmee ik dit vergeleek. De TypeScript-versie heeft 1.267 regels, de Go-versie 1.371 en de C#-versie 2.396. Tien van de elf gebruikte bibliotheken zijn geschreven door Paul Butcher. Claude Code en ik hebben gaandeweg fixes bijgedragen aan zes van deze bibliotheken.

3. Productie

Het slagen van tests op een laptop betekent niet dat een app klaar is voor echte gebruikers. De tweede vraag gaat over productie.

Vraag 2. Kan de implementatie van Theorem 1 echte gebruikers bedienen?

Er zijn twee problemen.

Opmerking 2 (Een jonge stack). De HTTP-server van Lean haalt maximaal een paar duizend verzoeken per seconde per proces. Dit komt grotendeels door een bug in de runtime van Lean, die inmiddels is opgelost maar nog niet is uitgebracht. Lean brengt bovendien elke maand een nieuwe versie uit, wat vaak bibliotheken breekt. Geen van beide problemen is relevant voor een kleine site die versies vastpind (pins).

Opmerking 3 (Wie heeft het geschreven). Bijna geen van deze code is met de hand geschreven; Claude Code schreef de app onder mijn leiding. De meeste bibliotheken zijn op dezelfde manier geschreven. Het is allemaal enkele maanden oud en heeft vaak slechts één of twee bijdragers. Code die zo snel is geschreven, is nog niet door veel lezers of gebruikers getest. Bugs die je alleen vindt bij echt gebruik, zitten er waarschijnlijk nog in.

De meest betrouwbare onderdelen zijn de types en de theorems, omdat Lean deze controleert. Deze blijven geldig ongeacht wie of wat de code heeft geschreven. De instructies die de bibliotheken aan hun AI-agent geven, stimuleren dit: ze vragen om "de sterkste vorm die een claim toelaat: een bewezen theorem over een eigenschap... over een voorbeeld en een verwacht resultaat". Ook is het gebruik van sorry als placeholder voor een ontbrekend bewijs verboden. Verschillende bibliotheken bevatten daadwerkelijke bewijzen. Code die niet door een theorem wordt gedekt, is slechts zo betrouwbaar als de tests. Voor bindings naar C-bibliotheken geldt dit dubbel, aangezien Lean de C-code helemaal niet kan controleren.

Toch moet je de bewezen delen nog steeds lezen. Lean controleert of elk bewijs correct is, maar kan niet controleren of het theorem daadwerkelijk beschrijft wat je nodig hebt. Agents die om bewijzen worden gevraagd, bewijzen vaak zaken die er niet toe doen. Toen Dan Luu coding-agents Zstd-compressie liet implementeren en hen vroeg Lean 4 te gebruiken, bewezen ze voornamelijk rekenkundige feiten terwijl ze de foutgevoelige code misten. Die bewijzen maakten de code niet correcter. Je moet dus alles lezen, inclusief theorems en bewijzen, om te controleren of het doet wat nodig is.

Tools zoals claimcheck kunnen hierbij helpen. Het gebruikt een AI-model om elk theorem in gewone taal te herformuleren zonder te weten wat het theorem oorspronkelijk bedoelde. Een tweede stap vergelijkt die herformulering met de oorspronkelijke bedoeling. Dit is een nuttige controle, maar vervangt het lezen niet.

Gedeeltelijk antwoord op Vraag 2. Kan de app echte gebruikers bedienen? Ja, mits aan drie voorwaarden wordt voldaan: (H1) het verkeer blijft bescheiden, (H2) je pint de toolchain, en (H3) iemand leest daadwerkelijk de code. De limieten van de server zijn niet relevant bij bescheiden verkeer. Je kunt ook meerdere kopieën van de app draaien voor meer belasting, omdat er geen staat tussen verzoeken wordt bewaard. Een gepinde toolchain voorkomt dat een nieuwe Lean-release zaken breekt voordat je besluit te upgraden. Het lezen van de code is haalbaar omdat de app slechts ongeveer 1.600 regels telt. Iemand zou de handlers, de SQL en de C-bindings zorgvuldig moeten lezen voordat echte gebruikers ze zien.

4. Correctheid

Ik geloof dat correctness by construction (correctheid door constructie) het doel moet zijn, vooral wanneer een AI het grootste deel van je code schrijft. Dit betekent dat je eerst exact vastlegt wat het programma moet doen in een formele taal. De code wordt vervolgens uit die beschrijving afgeleid via stappen die elk bewezen correct zijn.

Tegenwoordig vertrouwen de meeste mensen op tests, of geven een agent een specificatie in de hoop dat deze wordt gevolgd. Tests controleren alleen de gevallen waar iemand aan heeft gedacht. De experimenten van Dan Luu tonen aan dat agents slechte tests schrijven, zelfs wanneer ze instructies krijgen over welke techniek ze moeten gebruiken. Een specificatie op zichzelf kan niet aantonen dat de code deze daadwerkelijk volgt. Correctheid door constructie dicht dit gat, omdat Lean elke stap van specificatie naar code controleert. Het is de enige betrouwbare manier om kwalitatieve code te leveren terwijl je de snelheid van AI behoudt.

De laatste vraag is of deze app correct by construction zou kunnen zijn.

Definitie 2. Een programma is correct by construction als het is afgeleid van een formele specificatie via stappen die elk bewezen zijn de correctheid te bewaren.

Vraag 3. Is er een RealWorld-implementatie in Lean die correct by construction is?

Definitie 2 bestaat uit twee delen: een formele specificatie en een stapsgewijze afleiding daaruit.

  1. De specificatie. Heeft RealWorld een formele specificatie? Gedeeltelijk. Het contract is een OpenAPI-bestand plus de testsuites. Het OpenAPI-bestand is precies over de vormen (welke endpoints bestaan, welke velden ze accepteren en welke statuscodes ze retourneren). Wat de endpoints daadwerkelijk doen, is alleen in Engels beschreven. De tests concretiseren dit voor de specifieke gevallen die ze controleren. RealWorld is dus formeel over types, maar informeel over gedrag.
  2. De afleiding. Is de app afgeleid van die specificatie? Nee. Dat was een bewuste keuze. Omdat RealWorld alleen formeel is over types, is er niets precieers genoeg om het gedrag van de app uit af te leiden. Volledige correctheid door constructie was niet mogelijk met de huidige specificatie. Ik heb de app dus eerst geschreven en daarna getest.

In plaats daarvan heb ik een paar belangrijke eigenschappen geverifieerd. Drie hiervan worden gegarandeerd simpelweg omdat de code compileert.

Propositie 1. Als de types van een handler niet overeenkomen met de route, compileert de code niet.

Bewijs. lean-routing bepaalt het type van elke handler op basis van de route. Het OpenAPI-bestand stelt dat de id van een reactie een integer is. De routetabel zegt ook Nat. Een handler die de id als String accepteert, zal dus niet compileren:

error: Application type mismatch: The argument
deleteComment env
has type
String → String → Api.Handler
but is expected to have type
HandlerType Api.patterns.comment Result

Deze fout verschijnt tijdens het compileren, voordat de app start. ∎

Elke handler in Express of Go parseert de id zelf. Een mismatch in Rust’s axum wordt pas zichtbaar wanneer er een verzoek binnenkomt. Eén zwakke plek blijft: ik heb de routetabel handmatig gekopieerd vanuit het OpenAPI-bestand. Het automatisch genereren hiervan zou dit gat dichten.

Slugs tonen Definitie 2 op kleine schaal. Een slug is de URL-vriendelijke versie van een titel (bijv. hoe-train-ik-mijn-draak). RealWorld specificeert niet hoe een slug eruit moet zien, dus ik schreef eerst de specificatie als een Lean-type genaamd Valid. Een enkele kleine letter of cijfer is een geldige slug. Een geldige slug kan worden uitgebreid door een letter of cijfer ervoor te plaatsen, of een letter of cijfer gevolgd door een koppelteken. Alles wat anders is, is ongeldig. Dit sluit lege slugs, koppelteken aan het begin of einde, en dubbele koppeltekens uit. Een Slug is een string gebundeld met een bewijs dat deze aan deze regels voldoet:

inductive Valid : List Char → Prop where
| single {c} : isSlugChar c → Valid [c]
| cons {c rest} : isSlugChar c → Valid rest → Valid (c :: rest)
| hyphen {c rest} : isSlugChar c → Valid rest → Valid (c :: '-' :: rest)

structure Slug where
  toString : String
  valid : Valid toString.toList

Propositie 2. Elke slug die de app opslaat, is correct gevormd.

Bewijs. De functies die slugs opslaan, accepteren alleen een Slug-type, dus elke opgeslagen slug draagt zijn eigen bewijs mee. De meeste van deze bewijzen komen voort uit ofTitle, wanneer een titel wordt omgezet in een slug. Deze functie compileert alleen omdat er een bewijs bij zit dat het resultaat geldig is voor elke mogelijke titel. ∎

Hier is ofTitle. Het roept een helper aan, chars, die letters en cijfers behoudt, deze in kleine letters zet en alles daartussen omzet in enkele koppelteken. Vervolgens retourneert ofTitle die string samen met een bewijs dat deze geldig is. Het bewijs is het deel na by:

def ofTitle (title : String) : Slug :=
  match h : chars title.toList false false with
  | [] => ⟨"article", ...⟩   -- een titel zonder letters of cijfers
  | c :: cs =>
    ⟨String.ofList (c :: cs), by
      rw [String.toList_ofList, ← h]
      exact (chars_valid title.toList false).resolve_left (by rw [h]; exact List.cons_ne_nil _ _)⟩

Dit bewijs leunt op een lemma over chars. Dit lemma stelt dat chars voor elke titel ofwel niets, ofwel een geldige slug retourneert. Het lemma is bewezen via inductie over de tekens van de titel:

theorem chars_valid (cs : List Char) (pending : Bool) :
  chars cs false pending = [] ∨ Valid (chars cs false pending) := by
  induction cs generalizing pending with
  | nil => exact Or.inl rfl
  | cons c cs ih => ...

In totaal zijn dit ongeveer veertig regels bewijs voor tien regels code. Een property-based test zou een paar duizend willekeurige titels controleren; dit bewijs dekt elke titel, inclusief die welke nog nooit geschreven zijn.

Propositie 3. Tenzij de code Node.unsafeRaw aanroept, wordt alles wat een gebruiker typt ge-escaped voordat het op een pagina verschijnt.

Bewijs. Je kunt geen pagina-element in lean-html direct bouwen; alleen de functies van lean-html kunnen dat. Al deze functies, behalve Node.unsafeRaw, halen de tekst door escape. lean-html bewijst bovendien dat escape nooit een <, > of " in de output achterlaat:

def escapeChar (c : Char) : String :=
  match c with
  | '&' => "&amp;"
  | '<' => "&lt;"
  | '>' => "&gt;"
  | '"' => "&quot;"
  | c    => String.singleton c

theorem escape_safe (s : String) :
  ∀ c ∈ (escape s).toList, c ≠ '<' ∧ c ≠ '>' ∧ c ≠ '"' := ...

In gewone woorden: de ge-escapte versie van elke string bevat geen <, > of ". ∎

De website-tests van RealWorld controleren op cross-site scripting (XSS). Ze injecteren kwaadaardige tekst via de API en controleren of de pagina dit als platte tekst toont. De suite slaat deze tests over voor apps die zowel de API als de pagina's serveren, zoals deze app. Hier is het bewijs dus de enige controle. React escaped tekst op dezelfde manier, maar daar controleren tests of het escapen correct gebeurt.

Deze app is dus niet volledig correct by construction. Of er überhaupt een RealWorld-app in Lean kan zijn die dat wel is (Vraag 3), is nog onbeantwoord. Dat zou beginnen met het vastleggen van het gedrag van RealWorld in Lean. Het afleiden van de app daaruit zou ook een model van SQL vereisen, plus bewijzen over de C-bibliotheken en Std.Http die eronder liggen. Voor nu is de slug het enige onderdeel waar deze methode volledig is doorgevoerd.

***

Notities

  1. Alle 154 verzoeken van de API-suite slagen. De website-suite heeft 139 tests. Wanneer één app zowel de API als de site serveert, worden er 65 overgeslagen. De overige 74 slagen.
  2. De laatste stap van dit bewijs is het draaien van de twee testsuites, wat een berekening is. Bewijzen die eindigen in een computerrun hebben een lange geschiedenis (het vier-kleurentheorema is het bekendste voorbeeld). Dit bewijs gaat er ook van uit dat Postgres, een webbrowser en de test-runners correct werken, waardoor een strikte wiskundige het een experiment zou kunnen noemen.
  3. Niet-lege regels zonder commentaar, exclusief tests, voor nitro-prisma-zod, golang-gin en aspnetcore. De Lean-telling inclusief het SQL-schema en de bewijzen. De website voegt 616 regels toe. Het binary van 7,6 MB bouwt in 18 seconden op een M1, exclusief de bibliotheken.
  4. De README van de repository somt elke wijziging in de bibliotheek en de bijbehorende pull-request op.
  5. In Lean 4.34.1 handelt een kale Std.Http server die ok antwoordt ongeveer 1.800 verzoeken per seconde af bij 64 verbindingen. Go handelt er meer dan 100.000 af. De app zelf handelt er 1.170 tot 1.650 af, waarbij Postgres minder dan een halve core gebruikt. Het grootste gat komt door een bug in de async runtime van Lean. Deze is opgelost in lean4#15174 op 22 september 2026, maar is nog niet in een release opgenomen (ook niet in 4.35.0). Met de fix bereikt de kale server 8.640 verzoeken per seconde. Een enkele event-loop lock (lean4#13469) houdt het daarna nog ongeveer dertien keer trager dan Go. Gemeten op een Apple M1 met wrk gedurende tien seconden,取 de mediaan van drie runs.
  6. Reservoir is de package-index van Lean. Tussen 4.26 en 4.34 braken 9% van de packages zonder dependencies bij een release-update. Voor packages met dependencies was dit 23%. Beide cijfers laten packages die afhangen van Mathlib buiten. Release 4.34 alleen al brak vier van de hier gebruikte bibliotheken door een ontbrekende hernoeming. Geen enkele Rust-release in het jaar na 1.0 brak meer dan 1,3% van de crates.
  7. Lijsten van bijdragers op GitHub, oktober 2026.
  8. Dan Luu, "How well do agents use test and verification techniques?", september 2026. Hij draaide Codex met GPT-5.6 Sol ongeveer 80 keer voor elk van de 26 instructies, zoals "Use Lean 4" of "Use property-based testing". Alle implementaties waren in Rust. Agents die instructies kregen om andere formele tools te gebruiken, bewezen meestal ook irrelevante eigenschappen.
  9. claimcheck is gebouwd voor Dafny, een andere taal voor het bewijzen van programmacorrectheid. De repository voert dezelfde check uit op Lean 4-specificaties uit de VERINA-benchmark. De auteurs, Fernanda Graciolli en Nada Amin, beschrijven het als "een probabilistische sanity check die menselijke review en goedkeuring vereist".
  10. Het idee gaat terug naar E. W. Dijkstra, “A constructive approach to the problem of program correctness”, BIT 8 (1968). D. G. Kourie en B. W. Watson beschreven het als een methode in The Correctness-by-Construction Approach to Programming (Springer, 2012).
  11. Lean compileert een bewijs dat als sorry is gemarkeerd en geeft alleen een waarschuwing. De CI van de app wijst daarom elk theorem af dat op een sorry leunt.