Lean 4-webapp test de grens van formele garanties; C23-praktijk zet veiligheidsschakelaars aan

Een volledig in Lean 4 gebouwde RealWorld-webapp doorloopt volgens de maker de referentietests, maar bewijst slechts enkele afgebakende eigenschappen. Dat maakt het een bruikbare demonstratie van waar formele garanties in agent-geschreven software nu wel en niet reiken.

Daarnaast biedt een praktisch C23-verslag enkele kleine patronen om compilercontroles beter te benutten. Voor federatieve software is er een nieuw, bescheiden testinitiatief rond ActivityPub, waar interoperabiliteit nog altijd moeilijk te automatiseren blijkt.

Lean 4-webapp: tests slagen, maar slechts delen zijn formeel afgedekt

Een ontwikkelaar bouwde de bekende RealWorld-referentieapp — een Medium-achtige site met API- en browsertests — volledig in Lean 4, inclusief server-rendered frontend. De implementatie gebruikt onder meer Lean-bibliotheken voor HTTP, routing, JSON, PostgreSQL, JWT’s en HTML, met Datastar voor interactieve pagina-updates. Volgens de auteur slagen zowel de API- als websitetests.

Het interessante is niet dat dit meteen een productiestack vervangt, maar de scherp getrokken grens tussen testen en bewijzen. De auteur heeft bijvoorbeeld een Slug-type waarin elke opgeslagen slug een bewijs van geldigheid meedraagt, en een HTML-laag die gebruikersinvoer escapt tenzij een expliciete onveilige functie wordt aangeroepen. Lean controleert zulke eigenschappen bij elke build. De app is daarmee nadrukkelijk niet volledig ‘correct by construction’: de RealWorld-specificatie beschrijft gedrag deels alleen in gewone taal, en een volledig bewijs zou ook modellen en bewijzen voor SQL, C-bindings en de HTTP-runtime vragen.

Ook de productielimieten staan in het verslag zelf. De HTTP-runtime haalt volgens de maker voorlopig slechts enkele duizenden requests per seconde per proces wegens een runtimebug die al wel is gerepareerd maar nog niet vrijgegeven. Libraries zijn jong, maandelijkse Lean-releases kunnen breken en veel code is met Claude Code gemaakt en heeft weinig gebruikers of reviewers gehad. Een HN-reactie noemt bovendien hoge compileertijden bij een ander Lean-project; dat is een losse ervaring, geen meting van deze webapp.

De praktische les voor agent-ondersteunde software is bescheiden maar nuttig: types en formele eigenschappen kunnen precies omschreven invarianten sterker afdekken dan voorbeeldtests, maar ze maken de specificatie, afhankelijkheden en niet-bewezen businesslogica niet automatisch betrouwbaar. Technisch verslag en code-uitleg · HN-discussie

C23-praktijk: attributen, initialisatie en enumtypen als expliciete afspraken

Een C-ontwikkelaar beschrijft drie conventies die hij met -std=c23 in een bestaand project toepast. Ten eerste combineert hij [[nodiscard]] met [[maybe_unused]]: een returnwaarde moet standaard worden verwerkt, maar een uitzonderlijke bewuste negering blijft zichtbaar in de bron in plaats van achter een eigen UNUSED-macro te verdwijnen.

Verder wijst het verslag op het verschil tussen gedeeltelijke initialisatie en de in C23 beschikbare lege initialisatie { }, vooral bij structs met unions. De auteur kiest voor die laatste vorm om de volledige struct te nulinitialiseren. Als derde legt hij bij bitflag-enums het onderliggende type expliciet vast, bijvoorbeeld enum options : int, om niet stilzwijgend van integerrepresentatie te veranderen wanneer enumwaarden buiten int vallen.

Dit zijn geen universele migratievoorschriften en de post is geen vervanging voor de standaardtekst, compilerdocumentatie of eigen compatibiliteitstests. Maar het is wel een bruikbare reviewcheck voor teams die C23 inschakelen: maak bewust genegeerde resultaten, initialisatiegedrag en enumgrootte expliciet, en controleer daarna daadwerkelijk de gebruikte compiler- en warningconfiguratie. C23-conventies met voorbeelden · Lobsters-discussie

Verder nog

• ActivityPub-tests verzamelen lastige interoperabiliteitsgevallen: ActivityBot-werk bundelt volgens de auteur tests en voorbeelden van berichten en HTTP-signatures die andere projecten kunnen hergebruiken. De post laat tegelijk zien waarom unit-tests niet genoeg zijn: identifierregels en berichtschema’s zitten verspreid over specificaties, signatureverificatie vraagt echte voorbeelden, en ontvangen berichten vergen controle over een externe server. Zie het als gedeeld testmateriaal in opbouw, niet als een complete compliance-suite. Uitleg en testmateriaal · Lobsters-discussie