Lasm: Компилятор Lean 4 в WebAssembly для Node, serverless, edge и браузера.
Компилятор Lean 4 в WebAssembly для Node, serverless, edge и браузера.
Главное в цифрах
- Создатели: Millillion (владелец репозитория на GitHub; имя автора не указано)
- Стадия: показан на Hacker News
Как это работает
Компилирует обычные программы на Lean 4 в WebAssembly и запускает их на Node, Cloudflare Workers, Bun, Deno, WASI и в браузере. Пример Conduit содержит 117 доказанных теорем о коде, который реально работает.
Почему мы это показываем
Оригинальный подход и реальный пример с доказательствами и тестами в CI, но аудитория узкая, а интерес пока небольшой: около 50 звёзд на GitHub.
Источник: Show HN
Стартап-радар
Такие новости первыми, в Telegram