Lasm - Formally verified web apps in Lean for Node, serverless and edge
Show HN: Lasm – Write formally verified webapps in Lean for Node/serverless/edge
Lasm компилирует программы на Lean 4 в WebAssembly, позволяя создавать веб-приложения с математически доказанными свойствами. Одна кодовая база на Lean превращается в сервер Node, serverless- или edge-функцию, модуль WASI/Fastly или браузерное приложение. Флагманский пример Conduit — это RealWorld-приложение со 117 доказанными теоремами, охватывающими авторизацию, пагинацию, валидацию и безопасность Markdown. Lasm распространяется через npm и включает Lean, Lake и инструменты сборки; требуется только Node (или Bun, Deno). Начните с `npm create @lasm@latest my-app -- --template hono`, затем `cd my-app && npm install && npm run dev`.
Потому что это Lean, вы можете доказывать свойства кода, который развертываете.
- alexhixon
Интересно! Хотелось бы увидеть больше доказательств для фронтенда, например, у вас есть доказательства поведения, но ни одного о вёрстке или дизайне.
- orsorna
> Я инженер-агент с уклоном в программную инженерию
Это странно. Разве вы не считали бы себя программным инженером с уклоном в... агентную инженерию, или что-то в этом роде? Каков ваш опыт?
- sroerick
По-моему, это очень интересно, но что именно вы специфицируете, когда создаёте веб-сайт?
У меня ощущение, что это новый «разработка через тестирование» — идея совершенно хорошая, но не совсем полезная для самого процесса создания веб-приложений, где большинство ваших режимов отказа — это странный CSS, JS или проблемы с сервером.
Буду рад, если докажете, что я ошибаюсь.