Lasm
JavaScript 및 WebAssembly를 위한 Lean 4. Lasm은 일반적인 Lean 4 프로그램을 미리 WebAssembly로 컴파일합니다. 하나의 Lean 코드베이스만으로 Node 서버, 서버리스 또는 엣지 함수, WASI/Fastly 모듈, 그리고 브라우저 앱을 만들 수 있습니다. Lean 언어의 특성상 배포하는 코드의 속성을 증명할 수 있다는 장점이 있습니다. 대표적인 예시인 Conduit는 117개의 증명된 정리를 가진 RealWorld 앱입니다. Lasm은 npm을 통해 배포되며, Lean, Lake 및 빌드 도구를 함께 제공합니다. 사용자는 Node (또는 Bun 또는 Deno)만 필요합니다.
npm create @lasm@latest my-app -- --template hono
AI 에이전트 관련 정보: 이 README 파일만으로도 충분히 완벽합니다. llms.txt는 간략한 인덱스이며, docs/AI.md에는 잘못된 방향을 피할 수 있는 규칙들이 나열되어 있습니다.
Lasm이 유용하다면 후원해 주시면 감사하겠습니다 (더 보기).
주요 정보
| Fact | Value |
|---|
| Current version | @lasm/cli 0.3.5 (release notes); npm view @lasm/cli version |
| ... | |
플랫폼
모든 행은 해당 플랫폼의 로컬 런타임, 이미지 또는 에뮬레이터로 CI에서 테스트됩니다. 프로젝트 정책에 따라 CI는 실제 클라우드 계정에 배포하지 않습니다 (how each is tested).
| Deploy to | lasm build Main.lean --target … | Output | Since |
|---|
| Node server or program (any host, Docker/Kubernetes, Cloud Run, Fly.io, Railway, Render, Heroku, DigitalOcean) | node (default) | dist/ → node dist/main.mjs | 0.1.0 |
| ... | | | |
Node 빌드는 Lean의 전체 런타임(스레드, 파일, 프로세스, 소켓)을 갖추고 있습니다. 반면, 엣지(edge), Bun/Deno, WASI 및 브라우저 빌드는 스택이나 프로세스 없이 (WASI의 경우 파일을 제외하고도) 단일 스레드로 Lean을 실행하며, 나머지 Lean 기능은 정상적으로 작동합니다.
시작하기
플래그십 예제: Conduit (117개의 증명된 정리 포함)
examples/conduit는 Conduit([https://github.com/gothinkster/realworld])이며, RealWorld 앱(Medium 클론)으로, REST API, 서버 렌더링된 브라우저 앱 및 증명까지 모두 Lean으로 작성되었습니다.
- 117개의 정리: 실제로 실행되는 코드에 대한 증명으로,
sorry가 전혀 사용되지 않았고 Lean의 표준 공리만을 사용하여 검증되었습니다 (npm run proofs; PROOFS.md에 각 정리가 일반 영어로 나열되어 있습니다). 이 정리들은 권한 부여(작성자만 자신의 기사 및 댓글을 변경 가능), 팔로우 및 즐겨찾기, 충돌하지 않는 슬러그, 건너뛰거나 반복되지 않는 페이지네이션, 클라이언트와 서버가 공유하는 유효성 검사(앱은 서버가 거부할 내용을 절대 전송하지 않음), JSON 왕복 처리, Markdown 링크 안전성을 다룹니다. 엔드포인트는 함수의 Store를 기반으로 작성되었으며, 증명은 테이블 모델에서 동일한 코드를 실행합니다.
- 증명된 것이 아닌 신뢰하는 것: 각 SQL 구문이 모델에서 말하는 대로 작동한다는 점, JSON 텍스트 계층, 요청 간 동시성, 그리고 Lean, Lasm 및 JavaScript 런타임입니다. 전체 RealWorld 사양 준수 여부는 증명되는 것이 아니라 테스트됩니다.
- API: 공식 RealWorld API 스위트는 수정 없이 Node(
node:sqlite), Cloudflare Workers (D1), 그리고 Bun(bun:sqlite)에서 통과합니다. 각 대상에는 수동으로 작성된 @[js] 바인딩 모듈이 하나씩 있습니다.
- 프론트엔드: RealWorld의 공식 템플릿에 적용된
Lasm.UI로, 서버 측 렌더링(server-side rendering), 하이드레이션(hydration) 및 Lean에서 파싱되는 Markdown을 포함합니다. 공식 Playwright 엔드투엔드(end-to-end) 스위트는 Node 환경의 Chromium, Firefox, WebKit과 Workers 및 Bun 환경의 Chromium에서 재시도 없이 통과합니다.
이 모든 과정은 CI 환경(conduit.yml, run 40615274657에서 @lasm/cli 0.3.4 사용)에서 실행됩니다.
cd examples/conduit
npm install
npm run build && npm start
...
60초 시작
단일 파일만 있으면 프로젝트가 필요 없습니다. 이 전체 프로그램을 Main.lean으로 저장하세요:
def main : IO Unit := do
IO.println s!"Hello from Lean! 2 + 3 = {2 + 3}"
npx @lasm/cli Main.lean
npx @lasm/cli build Main.lean
새로운 기계에서 첫 번째 빌드를 수행하면 Lean과 빌드 도구가 한 번 다운로드됩니다(약 250–275 MB; Linux CI 러너에서 첫 빌드는 약 19초 소요). 이후의 개발 빌드는 한 줄 변경 사항에 대해 약 1~2초가 걸립니다.
레시피 (Recipes)
각 레시피는 생성, 개발, 빌드, 배포까지 완벽하게 갖추어져 있습니다. Lasm은 플랫폼 자체의 CLI(wrangler, vercel, fastly 등)를 설치하거나 시작하지 않습니다. 사용자가 직접 실행해야 합니다. npm run dev는 lasm dev와 같습니다: 저장할 때마다 약 2초 만에 재빌드하고 서버를 다시 시작하며, 타입 오류가 발생하더라도 마지막으로 성공했던 빌드를 유지합니다.
Node 서버 (Hono; 또한 express, fastify, std-http, fetch도 사용 가능).
npm create @lasm@latest my-api -- --template hono
cd my-api && npm install
npm run dev
...
AWS Lambda / Vercel / Netlify / Azure / Google Cloud Functions.
npm create @lasm@latest my-fn -- --template hono --deploy lambda-zip
cd my-fn && npm install
npm run build:lambda
...
Cloudflare Workers (및 Vercel Edge, Netlify Edge, Deno Deploy, Supabase).
npm create @lasm@latest my-edge -- --template hono --deploy workers
cd my-edge && npm install
npm run build:workers
...
Fastly Compute, WASI, Spin.
npm create @lasm@latest my-svc -- --template fetch --deploy fastly --deploy spin
cd my-svc && npm install
npm run build:fastly && fastly compute serve
...
브라우저 앱 (Browser app).
npm create @lasm@latest my-web -- --template web
cd my-web && npm install
npm run dev
...
풀 스택 (서버 + 브라우저 + 검증된 API).
npm create @lasm@latest my-app -- --template fullstack
cd my-app && npm install
npm run dev
...
에디터. 프로젝트당 한 번 npx lasm editor를 실행합니다. lasm init, lasm dev, 그리고 lasm build도 이 작업을 수행합니다. 이후 Lean 에디터(VS Code의 Lean 4 확장 프로그램)가 import Lasm.*를 해결합니다(자세히 보기).
전체 스택을 Lean으로, 검증된 방식으로 구현하기
fullstack 템플릿은 서버(Lasm.Fetch), 브라우저 앱(Lasm.UI), 그리고 이들 사이의 API(Lasm.RPC)를 포함하는 하나의 Lean 프로젝트입니다. 요청이 충족해야 하는 규칙은 양쪽 모두가 가져오는(import) Shared.lean에 한 번 작성되고 증명됩니다([templates/fullstack]):
-- Shared.lean
@[irreducible] def checkTitle (title : String) : Except String Unit :=
let n := (clean title).length
...
-- Server.lean: ToDo를 저장하려면 제목이 검사를 통과했다는 증명이 필요하며,
-- `addTodo.serve`는 재검증 후 핸들러에 해당 증명(`ok`)을 전달합니다.
def Store.add (s : Store) (title : String) (_ : checkTitle title = .ok ()) : Store × Todo :=
...
-- Client.lean: a theorem about the browser app: it never sends an invalid title.
theorem add_invalid (m : Model) (e : String) (h : checkTitle m.draft = .error e) :
(update .add m).2.effects = [.msg (.added (.error (.invalid e)))] :=
...
증명은 어디에 존재하며 어떻게 검사되는가.
| 증명 (Proof) | 위치 (Where) | 검증 주체 (Checked by) |
|---|
사용자의 정리들 (checkTitle_ok, add_invalid 등) | 사용자의 .lean 파일 | 모든 lasm build/lasm dev 실행 (Lean이 이를 전개(elaborates)하며, 증명이 깨지면 빌드 오류가 발생함); 순수 모듈의 경우 lake build도 포함 |
| ... | | |
증명되지 않고 대신 CI에서 테스트되는 부분: 클라이언트와 서버 간의 JSON/HTTP 전송, 실제 DOM에 패치를 적용하는 JavaScript, Lasm 컴파일러 및 런타임, 그리고 브라우저들. Lean 자체 컴파일러는 모든 Lean 프로그램과 마찬가지로 신뢰됨(UI.md, RPC.md).
JavaScript 및 npm 호출하기 (Calling JavaScript and npm from Lean)
호출하는 모든 JavaScript 함수는 한 줄로 선언하며, Lean 타입이 값들이 어떻게 변환되는지 알려준다. 완전한 프로그램(Node의 전역 fetch 등) 예시:
import Lasm.JS
open Lasm.JS
...
바인딩을 작성하는 규칙:
- @[js "module" "export"] opaque name : A → B → IO R
는 module.export를 바인딩합니다. 이 모듈은 npm 패키지("marked"), Node 내장 모듈("node:fs"), 또는 전역 변수를 위한 "globalThis"일 수 있습니다. "new Hono"는 생성자를 호출하며, ""`는 모듈 자체의 값입니다.
- 즉시 반환되는 값에는 타입을
IO R로, Promise에 대해서는 Async R로 끝냅니다. Async 바인딩은 Lean 스레드를 유지하지 않고 await됩니다.
String, Nat, Int, Float, Bool, ByteArray, Array, List, Option, 튜플, Data (모든 JS 데이터) 또는 Value (JS 객체 참조: get, callMethod, callMethodAwait)를 사용합니다. 사용자 정의 구조체는 deriving ToJS, FromJS로 변환됩니다.Function.ofFn / Function.ofFnReply는 Lean 함수를 JS 콜백으로 변환합니다. 프레임워크 핸들러에서 사용됩니다 (hono, express 및 fastify 템플릿 참조).- 패키지를 lakefile 옆에
npm install합니다. lasm build는 설치된 패키지와 모든 바인딩을 확인하고 (Lasm.JS binding check failed: … export "x" is missing), 프로덕션 종속성을 dist/node_modules로 복사합니다.
- 각 호출은 Lean 스레드에서 Node의 메인 스레드로 전환됩니다 (약 24 µs). 따라서 여러 개의 작은 호출보다는 하나의 큰 호출을 선호하세요.
Express, Hono, pg, jose 및 fetch 예제와 에이전트 체크리스트가 포함된 전체 가이드: docs/JS_BINDINGS.md.
측정된 수치
다른 실행이 명시되지 않은 경우, 모든 수치는 무료 GitHub runner(4-CPU AMD EPYC, Linux x64)의 CI에서 측정된 것입니다. 후보 버전은 0.1.0-experimental.40494203854 (2026-10-27)입니다.
전체 표, 방법 및 주의사항: BENCHMARKS.md.
| 항목 | 수치 |
|---|
| Node: Hono + Lean handler, 콜드 스타트부터 첫 HTTP 응답까지 | 159 ms (일반 Node http: 4.1배 빠름) |
| ... | |
Lean을 노드(Node) 환경에서 사용하려면 WebAssembly와 스레드를 활용합니다. 콜드 스타트(cold start)는 CPU에 의해 제한되므로, 작은 서버리스 CPU 공유에서도 성능이 저하될 수 있으며, 모든 JavaScript 호출은 스레드를 가로지릅니다. 순수 Lean의 Std.Http는 노드에서 느리므로 (1,290 req/s), 프로덕션 HTTP에는 Hono, Express, Fastify 또는 Lasm.Fetch를 사용해야 합니다. 수천 자리 숫자에 대한 산술 연산은 네이티브 Lean보다 느립니다 (GMP 없음). | |
알려진 제한 사항 (Known limitations)
- 오직 사전 컴파일(Ahead of time)만 가능. 배포된 프로그램은 Lean을 확장하거나, 평가하거나, 컴파일할 수 없으며, 모듈 데이터나 플러그인을 로드하거나, 런타임에 Lean의 C++ 컴파일러/커널을 사용할 수 없습니다. (정확한 목록 참조)
- 정확히 Lean 4.35.0 버전만 지원. 다른
lean-toolchain 버전은 메시지와 함께 거부됩니다.
- Node: 앱에 최소 512MB를 할당해야 합니다. 약 22GB의 가상 주소 공간을 예약하기 때문입니다. 미리 빌드된 네이티브 라이브러리(
-l, 공유 라이브러리)는 링크할 수 없으며, 패키지에 포함된 C 소스 코드는 컴파일되어야 합니다.
- Edge, Bun/Deno, 브라우저, WASI: 단일 스레드 Lean입니다. 소켓(sockets), 프로세스 또는 시그널(signals)이 없고, WASI에서만 파일에 접근할 수 있습니다. 브라우저에서는
--suspend jspi로 빌드된 경우를 제외하고는 블로킹 대기(blocking waits)가 앱을 멈추게 하므로 Async를 사용해야 합니다.
- npm 패키지에 대한 미리 만들어진 바인딩이 없습니다. 핵심 웹 플랫폼은
Lasm.Web이 담당합니다.
- 에디터: 에디터에서
npx lasm editor를 실행한 후, Lasm.* 임포트는 해결됩니다.
- 플랫폼: Windows ARM64와 Alpine/musl 빌드 머신은 지원하지 않습니다 (빌드된 앱은 Alpine에서 실행됨). 호스팅 플랫폼은 실제 계정으로는 테스트되지 않고 로컬 도구로만 테스트되었습니다.
문서화