Lasm, Lean 4 programlarını Node, serverless, edge ve tarayıcı hedefleri için WebAssembly'e derliyor

MIT lisanslı yeni araç zinciri Lasm, alışılmadık bir vaatle Hacker News'in ana sayfasına ulaştı: web uygulamanızı Lean 4 ile yazın, davranışı hakkında teoremler kanıtlayın, ardından aynı doğrulanmış kodu neredeyse tüm mainstream JavaScript veya WebAssembly runtime'larına dağıtın.

GitHub'daki proje README'sine göre Lasm, normal Lean 4 kaynak kodunu alıyor ve ahead of time olarak WebAssembly'e derliyor. Tek bir kod tabanı daha sonra bir Node sunucusu, bir AWS Lambda fonksiyonu, bir Cloudflare Worker, bir Fastly Compute veya WASI servisi ya da statik bir tarayıcı uygulaması olarak paketlenebiliyor. Güncel sürüm @lasm/cli 0.3.5.

Lean bir npm paketi olarak geliyor

Geliştiricilerden Lean araçlarını elle kurmalarını istemek yerine Lasm, npm üzerinden dağıtılıyor ve Lean'ı, onun build aracı Lake'i ve derlemek için gereken diğer her şeyi birlikte sunuyor. Tek ön koşul Node 24 veya daha yeni bir sürüm, ya da Bun ya da Deno. Araç zinciri Lean'ı tam olarak 4.35.0 sürümüne sabitliyor ve ayrı bir elan kurulumu gerekmiyor. Yeni projeler npm create @lasm@latest ile başlıyor; Hono, Express veya Fastify üzerine kurulu API'ler, saf-Lean sunucular, tarayıcı uygulamaları ve full-stack uygulamalar için şablonlar mevcut.

Derleme işlemleri, program.wasm ve Node için bir JavaScript başlatıcısı içeren bir dist klasörü üretiyor ya da bir --target bayrağı geçildiğinde platforma özgü bir paket oluşturuyor. Derleme ahead of time gerçekleştiği için Lean'ın etkileşimli katmanı build zamanında geride kalıyor: README, elaboration, #eval tarzı değerlendirme, .olean yükleme ve Lean kernel'inin runtime'da hiçbirinin kullanılamadığını belirtiyor.

Geniş bir dağıtım matrisi

README; herhangi bir ana makinede Node (Docker, Kubernetes, Cloud Run, Fly.io ve diğerleri), hem zip hem container biçiminde Lambda ve Lambda@Edge, Vercel, Netlify, Azure ve Google Cloud'daki fonksiyonlar, Cloudflare Workers, Vercel Edge, Netlify Edge, Deno Deploy ve Supabase dahil edge runtime'ları, ayrıca Bun, Deno, Fastly Compute, WASI, wasi-http ve dört büyük tarayıcıyı kapsayan hedefleri belgeliyor. Her satır, CI'da platformun yerel runtime'ı, imajı veya emülatörü karşısında sınanıyor ve proje politikası gereği CI asla gerçek bir bulut hesabına dağıtım yapmıyor.

Yetenekler hedefe göre farklılaşıyor. Node derlemeleri thread'ler, dosyalar, süreçler ve socket'ler dahil Lean'ın tam runtime'ını alıyor. Edge, Bun/Deno, WASI ve tarayıcı derlemeleri tek thread'li ve socket ile süreç desteğinden vazgeçiyor; ayrıca WASI dışında her yerde dosya erişimi de yok.

Lean ile yazılmış framework'ler

Lasm kendi kütüphanelerini de sağlıyor: her sunucu hedefinde HTTP için Lasm.Fetch, kanıtlanmış bir diff algoritmasıyla Elm tarzı bir mimari kullanan tarayıcı arayüzleri için Lasm.UI, tipli client/server API'leri için Lasm.RPC, DOM ve web API'leri için Lasm.Web ve key-value depolama için Lasm.KV.

npm ile birlikte çalışabilirlik otomatik değil, isteğe bağlı. Lasm.JS'i içe aktardıktan sonra çağırmak istediğiniz her JavaScript fonksiyonu tek bir @[js] ek açıklamasına ihtiyaç duyuyor; hazır binding'ler yok ve Conduit örneği hedef başına yalnızca elle yazılmış tek bir binding modülü kullanıyor.

Conduit: 117 kanıtlanmış teorem

Amiral gemisi örnek, tamamen Lean ile yazılmış standart RealWorld Medium klonu Conduit: REST API, hydration ile sunucu tarafında render edilen ön yüz ve kanıtlar. README, dağıtılan kod hakkında sorry yer tutucusu olmadan ve yalnızca Lean'ın standart aksiyomlarıyla doğrulanmış 117 kanıtlanmış teorem bildiriyor. Bu teoremler; yalnızca bir makalenin yazarının onu veya yorumlarını düzenleyebileceğini, slug'ların asla çakışmayacağını, sayfalamanın asla kayıt düşürmeyeceğini veya kayıt çoğaltmayacağını ve client ile server'ın tek bir doğrulayıcı paylaştığını — dolayısıyla ön ucun, arka ucun reddedeceği bir şeyi asla göndermeyeceğini — JSON gidiş-dönüş ve Markdown bağlantı güvenliği garantilerinin yanında ortaya koyuyor.

README, kanıtlanan değil güvenilen kalan kısımlar hakkında açık sözlü: her SQL ifadesinin modeline uyduğu varsayımı, JSON metin katmanı, istekler arasındaki eşzamanlılık ve Lean, Lasm ile JavaScript runtime'ının kendisi. Tam RealWorld spesifikasyonuna uygunluk kanıtlanmıyor, test ediliyor. Resmi API paketi değiştirilmeden geçiyor — 13 dosyanın 13'ü, 154 istek — Node, Cloudflare Workers ve Bun üzerinde; resmi Playwright uçtan uca paketi ise Node üzerinde Chromium, Firefox ve WebKit'te yeniden denemesiz geçiyor.

Neden önemli

Formal doğrulama nadiren araştırma ve güvenlik-kritik nişlerden dışarı çıkıyor; bunun başlıca nedeni, kanıt yapabilen dillerin sıradan dağıtım için bir hikâyesinin olmaması. Lasm'ın bahsi, WebAssembly'nin bunu sağlayabileceği: doğrulanmış Lean kodu her büyük sunucu ve tarayıcı platformunda yerel olarak çalışırsa, doğrulanmış web servisleri yazmanın pratik maliyeti ciddi biçimde düşer. Conduit hem tavanı hem tabanı gösteriyor — yetkilendirme kuralları gibi gerçek değişmezler kanıtlanırken, SQL semantiği, eşzamanlılık ve runtime güvenilen tarafta kalıyor. Yine de, doğrulanmamış yüzeyi kısa ve belgelenmiş bir listeye sıkıştırmak, bugün bu yüzeyin fiilen her şey olduğu web geliştirme için anlamlı bir yükseltme olurdu.