1 неделю назад
Lasm компилирует Lean 4 в WebAssembly для Node и edge-функций
Lasm, проект, который заранее (ahead of time) компилирует обычные программы на Lean 4 в WebAssembly. Из одной кодовой базы на Lean можно получить сервер на Node, serverless- или edge-функцию, модуль для WASI/Fastly или браузерное приложение. Поскольку это Lean, говорится в README, можно доказывать свойства кода, который вы разворачиваете. Lasm выходит на npm и приносит с собой Lean, Lake и инструменты сборки; из окружения нужен только Node (или Bun, или Deno). Проект создаётся командой npm create @lasm@latest my-app -- --template hono...