Lasm：用 Lean 4 编写可形式化验证的 Web 应用，编译到 Node、Serverless 与边缘平台
Show HN: Lasm – Write formally verified webapps in Lean for Node/serverless/edge
Lasm 将普通 Lean 4 程序提前编译为 WebAssembly，同一份代码可部署为 Node 服务器、Serverless 或边缘函数、WASI/Fastly 模块及浏览器应用，并支持对部署代码进行性质证明。
Show HN: Lasm – Write formally verified webapps in Lean for Node/serverless/edge
Lasm 将普通 Lean 4 程序提前编译为 WebAssembly，同一份代码可部署为 Node 服务器、Serverless 或边缘函数、WASI/Fastly 模块及浏览器应用，并支持对部署代码进行性质证明。