Lasm - Formell verifizierte Webapps in Lean für Node, Serverless und Edge
Show HN: Lasm – Write formally verified webapps in Lean for Node/serverless/edge
Lasm kompiliert gewöhnliche Lean-4-Programme vorab zu WebAssembly – eine Codebasis wird so zum Node-Server, zur Serverless- oder Edge-Function, zum WASI/Fastly-Modul oder zur Browser-App. Weil es Lean ist, lassen sich Eigenschaften des deployten Codes beweisen: Das Flaggschiff-Beispiel Conduit, eine vollständige RealWorld-App, bringt 117 bewiesene Theoreme mit, die etwa Autorisierung, Pagination und Validierung abdecken. Installation und Start laufen über npm, benötigt wird nur Node (oder Bun/Deno). Wer schon immer formale Garantien in seinen Web-Stack bringen wollte, kann mit einem einzigen Befehl loslegen.
Weil es Lean ist, kannst du Eigenschaften des Codes beweisen, den du tatsächlich deployst.
- alexhixon
Interessant! Ich hätte gerne mehr Frontend-Beweise gesehen, zum Beispiel hast du Beweise über Verhalten, aber keine über Layout oder Design.
- orsorna
> Ich bin ein agentischer Ingenieur mit Schwerpunkt auf Software-Engineering
Das ist seltsam. Würdest du dich nicht als Software-Ingenieur mit Schwerpunkt auf ... agentischem Engineering oder so etwas betrachten? Was ist dein Hintergrund?
- sroerick
Ich finde das sehr interessant, aber was spezifizierst du, wenn du eine Website baust?
Ich habe das Gefühl, das ist das neue "testgetriebene Entwicklung", was total eine gute Idee ist, aber auch nicht ganz nützlich für den eigentlichen Prozess des Bauens von Web-Apps, wo die meisten deiner Fehlermodi seltsames CSS, JS oder Serverprobleme sind.
Ich würde mich freuen, eines Besseren belehrt zu werden.