Medium-klone beviser 117 koderegler med værktøjet Lasm

En udvikler har bygget Conduit, en Medium-klone, hvor 117 matematiske beviser viser, at koden lever op til reglerne. Det betyder, at man kan stole på, at programmet opfører sig korrekt, ikke kun at testerne består. Værktøjet Lasm, der gør det muligt, udkommer nu i version 0.3.5 og kan installeres gratis via npm.

Forestil dig, at du kunne bevise matematisk, at din blog aldrig ville gå i stykker på de måder, du frygter. Det er præcis, hvad Conduit er: en klon af Medium, skrevet i programmeringssproget Lean, hvor man kan skrive beviser for, at koden opfører sig, som den skal. Projektet indeholder 117 sådanne beviser. Én af dem viser, at kun forfatteren kan redigere sine egne artikler og kommentarer. Andre viser, at korte webadresser aldrig kolliderer, og at opdelingen af indlæg i sider aldrig springer et indlæg over eller gentager et. Hvert bevis er forklaret i almindelige ord i projektets PROOFS.md-fil.

Conduit er flagskibseksemplet bag Lasm, et værktøj, der oversætter almindelige Lean 4-programmer til WebAssembly — et format, som browsere og mange servere kan køre. Tænk på det som en bro: Lean-verdenens strenge beviser bliver brugbare i helt almindelige webapps. Én kodebase kan blive til en Node-server, en serverless- eller edge-funktion (små programmer, der kører hos en udbyder), et Fastly-modul eller en browserapp. Lasm udkommer i version 0.3.5 under MIT-licensen og installeres via npm, JavaScript-verdenens pakkeværktøj. Værktøjet bringer Lean og dets byggeværktøjer med sig, så du kun behøver Node, Bun eller Deno — tre populære måder at køre JavaScript på. En skabelon med webframeworket Hono starter et nyt projekt med én kommando, og en enkelt fil kan bygges uden et helt projekt.

Beviserne gælder koden, der faktisk kører. De dækker også validering delt mellem klient og server, så appen aldrig sender noget, serveren ville afvise — lidt som at tjekke adressen på kuverten, før du sender brevet. Derudover dækker de JSON-rundture (data udvekslet frem og tilbage i et tekstformat) og sikre Markdown-links. Men der er grænser: At hver SQL-sætning gør, hvad dens model lover, JSON-tekstlaget, samtidighed mellem forespørgsler samt Lean, Lasm og JavaScript-runtime'en er betroet, ikke bevist. At appen overholder hele RealWorld-specifikationen er testet, ikke bevist.

I praksis virker det: Den officielle RealWorld-testsuite består uændret af 154 forespørgsler på Node, Cloudflare Workers og Bun, og Playwright-testen kører uden genforsøg i Chromium, Firefox og WebKit. Node-bygget har Leans fulde runtime med tråde, filer og sockets, mens edge-, Bun-, Deno- og browser-byggene kører enkelttrådet uden sockets og processer. En pris skal man dog betale: Lasm har ingen færdige bindinger til JavaScript-biblioteker, så hver funktion, du kalder, kræver én håndskrevet linje i koden.