Lasm – Lean asosida formal tasdiqlangan web ilovalar uchun yangi kompilyator

Lasm - bu Lean 4 dasturlash tilini JavaScript va WebAssembly dunyosiga olib kiruvchi inqilobiy platforma. Bir nechta buyruq bilan Lean kodini Node serveri, serverless funksiyasi, edge xizmat yoki brauzer ilovasi sifatida paketlash mumkin. Formal tasdiqlash imkoniyati esa kodning ishonchliligini matematik jihatdan kafolatlaydi.

Qisqa tarix va motivatsiya

Lean 4 ilmiy va akademik sohalarda isbotlash uchun keng qo'llanilayotgan interaktiv teorem prover bo'lib, ammo uning amaliy web dasturlarga qo'llanilishi cheklangan edi. Lasm bu bo'shliqni to'ldirish maqsadida yaratilgan; u Lean 4 ni WebAssembly ga oldindan kompilyatsiya qiladi va shu bilan birga npm paketlari orqali oson integratsiyani ta'minlaydi. Natijada dasturchilar bir kod bazasidan bir nechta platforma uchun bir xil tasdiqlangan ilovalarni yaratish imkoniga ega bo'ladilar.

npm create @lasm@latest my-app -- --template hono    # then: cd my-app && npm install && npm run dev

Asosiy funksiyalar va texnik tafsilotlar

Lasm quyidagi asosiy komponentlardan iborat:

cd examples/conduit
npm install                                   # @lasm/cli, Hurl and Playwright (the official suites' runners)
npm run build && npm start                    # http://localhost:3000: the app and its API on Node
npm run proofs                                # check all 117 theorems
npm test                                      # the official API suite (also test:workers, test:bun)
npx playwright install chromium && npm run test:e2e   # the official end-to-end suite
npm run build:workers && npx wrangler dev     # Cloudflare Workers with local D1
npm run build:bun && npm run start:bun        # Bun with bun:sqlite

• Lean 4 integratsiyasi – Lasm o'z ichiga Lean 4.35.0 versiyasini oladi, shuning uchun foydalanuvchi alohida elan o'rnatishi shart emas.
• WebAssembly chiqishi – kompilyatsiya qilingan kod dist/ papkasida program.wasm va JavaScript launcher bilan birga keladi.
• Platforma shablonlari – hono, fetch, std-http, web, fullstack kabi shablonlar yordamida Node, serverless, edge, WASI, Fastly, Cloudflare Workers, Vercel, Netlify, Azure, Google Cloud Functions, Deno Deploy, Supabase Edge kabi muhitlarga bir necha bosqichda deploy qilish mumkin.
• JS/npm integratsiyasi – import Lasm.JS; @[js "pkg" "export"] sintaksisi orqali har bir Lean funksiyasini JavaScript paketiga bog'lash mumkin, oldindan tayyor bindinglar talab qilinmaydi.
• Formal tasdiqlash – Conduit misolida ko'rinishicha, RealWorld ilovasi 117 ta teorem bilan tasdiqlangan, bu esa ishlab chiqish jarayonida xatoliklarni oldindan aniqlashga yordam beradi.

Lasm npm paketlari sifatida @lasm/cli va @lasm/create ni taqdim etadi. O'rnatish uchun npm install -D @lasm/cli yoki npx @lasm/cli … buyruqlari kifoya. Yangi loyiha yaratish npm create @lasm@latest my-app -- --template hono kabi oddiy buyruqlar bilan amalga oshiriladi.

def main : IO Unit := do
  IO.println s!"Hello from Lean! 2 + 3 = {2 + 3}"

Platforma va ishga tushirish talablari

Lasm Linux x64/arm64, macOS x64/arm64 va Windows x64 muhitlarida ishlaydi. Kompilyatsiya vaqtida Node 24 yoki undan yuqori versiyasi, shuningdek Bun 1.4.4 va Deno 2.9.6 sinovdan o'tgan. Edge va WASI qurilmalarida Lean yadro funksiyalari (elaboration, #eval, .olean yuklash) faqat build vaqtida mavjud bo'lib, runtime da yo'q; bu xavfsizlik va resurslarni tejashga xizmat qiladi.

npx @lasm/cli Main.lean          # builds and runs: Hello from Lean! 2 + 3 = 5
npx @lasm/cli build Main.lean    # writes dist/; run it with: node dist/main.mjs

Raqobatchilar bilan taqqoslash

Hozirgi kunda WebAssembly ga Lean kodini kompilyatsiya qiluvchi bir necha loyiha mavjud, lekin ularning aksariyati qo'shimcha qurilmalar (elan) talab qiladi yoki tasdiqlash imkoniyatini taqdim etmaydi. Masalan, lean-wasm loyihasi Lean kodini WASM ga o'girishni qo'llab-quvvatlasa-da, tasdiqlashni integratsiyalashmagan. Lasm esa bir paketda Lean, Lake, build tools va npm integratsiyasini birlashtiradi, shu bilan birga tasdiqlashni ham avtomatik ravishda qo'shadi.

npm create @lasm@latest my-api -- --template hono
cd my-api && npm install
npm run dev                                   # http://localhost:3000/hello/Ada
npm run build && npm start                    # dist/ needs only Node 24+
docker build -t my-api . && docker run -p 8080:8080 my-api   # the generated Dockerfile

Shuningdek, traditsion JavaScript/TypeScript frameworklari (Express, Fastify, Hono) bilan Solana, Rust, Go kabi tillar orasidagi farqni ham ko'rish mumkin. Lasm bu farqni Lean ning kuchli tip tizimi va isbotlash imkoniyatlari bilan birlashtiradi, natijada kodning funksional to'g'riligi va xavfsizligi yuqori darajada bo'ladi.

npm create @lasm@latest my-fn -- --template hono --deploy lambda-zip   # or vercel, netlify, azure, gcf, lambda-edge
cd my-fn && npm install
npm run build:lambda                          # dist/ and lambda.zip (handler lasm-lambda.handler)
# deploy lambda.zip with the AWS console, aws CLI or SAM; recipes: docs/deploy/lambda.md

Cheklovlar va ochiq savollar

Lasm hali ham rivojlanish bosqichida bo'lgani sababli ba'zi cheklovlarga ega. Birinchidan, runtime da Lean ning to'liq yadro funksiyalari (masalan, fayl tizimi, socketlar) cheklangan; bu esa ba'zi murakkab server ilovalarini yaratishda qo'shimcha kutubxonalar talab qilishi mumkin. Ikkinchidan, tasdiqlash jarayoni dasturchidan qo'shimcha teoremlar yozishni talab qiladi, bu esa o'rganish egri chizig'ini biroz keskin qiladi.

npm create @lasm@latest my-edge -- --template hono --deploy workers
cd my-edge && npm install
npm run build:workers                         # workers/ (wrangler.toml came from lasm init)
npx wrangler dev                              # local workerd; npx wrangler deploy to publish

Kelajakda Lasm qanday qilib ko'p platformali fayl tizimi, socket va jarayonlarni qo'llab-quvvatlashni kengaytirishi, hamda tasdiqlash jarayonini avtomatlashtirishga yo'naltirilgan vositalar (masalan, proof generation wizard) yaratishi kutilmoqda.

npm create @lasm@latest my-svc -- --template fetch --deploy fastly --deploy spin
cd my-svc && npm install
npm run build:fastly && fastly compute serve  # Viceroy on http://127.0.0.1:7676
npm run build:wasi-http && spin up            # or: wasmtime serve wasi-http/main.wasm

Kimga va qanday ta'sir qiladi?

Lasm asosan quyidagi auditoriyaga mo'ljallangan:

• Formal tasdiqlashga qiziqqan dasturchilar va ilmiy tadqiqotchilar.
• WebAssembly asosida yuqori samarali, xavfsiz serverless yoki edge funksiyalarini yaratmoqchi bo'lgan kompaniyalar.
• Lean 4 ni amaliy dasturlashga qo'llashni istagan universitetlar va o'quv markazlari.

Ushbu guruhlar Lasm orqali kodning ishonchliligini oshirish, test va debugging xarajatlarini kamaytirish, hamda bir kod bazasidan ko'p platforma uchun bir xil ilova yaratish imkoniyatiga ega bo'ladilar.

Xulosa

Lasm Lean 4 ning kuchli tip tizimi va isbotlash imkoniyatlarini WebAssembly, Node, serverless va edge muhitlariga olib keladi. Bir nechta platforma shablonlari, npm integratsiyasi va tasdiqlashni birlashtirgan holda, u dasturchilarga yuqori darajadagi ishonchlilik va ko'p platformali tarqatish imkoniyatini taqdim etadi. Hozirgi cheklovlar mavjud bo'lsa-da, loyiha faol rivojlanmoqda va kelajakda yanada kengaytirilgan funksiyalar kutilmoqda. Formal tasdiqlashni amaliy web dasturlarga qo'shish istagida bo'lgan har bir dasturchi Lasmni sinab ko'rishi lozim.

Asl manba: github.com