Lasm - Escribe webapps con verificación formal en Lean para Node, serverless y edge
Show HN: Lasm – Write formally verified webapps in Lean for Node/serverless/edge
Lasm compila programas Lean 4 a WebAssembly, permitiendo que una sola base de código se convierta en servidor Node, función serverless, edge function o app de navegador. Su gran ventaja es que puedes demostrar propiedades del código que despliegas: el ejemplo estrella, Conduit (un clon de Medium), incluye 117 teoremas verificados sobre autorización, paginación y validación. Se instala vía npm sin necesidad de configurar Lean manualmente, soporta frameworks como Hono, Express y Fastify, y despliega en Cloudflare Workers, AWS Lambda, Vercel, Fastly y más. Ideal para equipos que quieren la seguridad de la verificación formal sin abandonar el ecosistema JavaScript.
Como está hecho en Lean, puedes demostrar propiedades del código que despliegas: el ejemplo estrella, Conduit, es la app RealWorld con 117 teoremas demostrados.
- alexhixon
¡Interesante! Me habría encantado ver más pruebas de frontend, por ejemplo tienes pruebas sobre el comportamiento pero ninguna sobre el layout o el diseño.
- orsorna
> Soy un ingeniero agéntico con énfasis en ingeniería de software
Esto es raro. ¿No te considerarías un ingeniero de software con énfasis en... ingeniería agéntica, o algo así? ¿Cuál es tu formación?
- sroerick
Creo que esto es muy interesante, pero ¿qué estás especificando cuando construyes un sitio web?
Siento que esto es el nuevo "desarrollo guiado por pruebas", lo cual es totalmente una buena idea, pero también no es del todo útil para el proceso real de construir aplicaciones web, donde la mayoría de tus modos de fallo son CSS, JS o problemas del servidor extraños.
Aunque me encantaría que me demostraran que estoy equivocado.