Lasm proporciona un puente entre la verificación formal y el despliegue web moderno al permitir que los desarrolladores escriban aplicaciones en Lean 4 —un lenguaje de programación funcional y demostrador de teoremas— y las compilen en WebAssembly (Wasm). A diferencia del desarrollo web estándar, donde la lógica se verifica principalmente mediante pruebas unitarias, Lasm permite el uso de pruebas formales para garantizar que el código se comporte correctamente de acuerdo con reglas específicas. Este enfoque permite a los desarrolladores demostrar propiedades como la lógica de autorización, la validación de datos y la consistencia de la paginación antes de que el código sea desplegado.
La imagen representa la funcionalidad principal de la cadena de herramientas Lasm para Lean 4 y WebAssembly.
La cadena de herramientas admite una amplia gama de objetivos de despliegue, incluidos Node.js, AWS Lambda, Vercel y Cloudflare Workers. Gestiona las complejidades de los diferentes entornos de ejecución proporcionando objetivos de construcción específicos para cada uno. Por ejemplo, mientras que las construcciones de Node.js pueden utilizar todas las características del entorno de ejecución de Lean, como hilos y sockets, las construcciones para el borde (edge) y el navegador están optimizadas para ejecutarse en un solo hilo sin esas capacidades específicas. Lasm también proporciona un conjunto de bibliotecas, como Lasm.Fetch para solicitudes HTTP y Lasm.UI para interacciones en el navegador, para facilitar la creación de aplicaciones full-stack manteniendo la capacidad de verificar la lógica subyacente.
Una característica clave de Lasm es su capacidad para compartir lógica verificada entre el cliente y el servidor. Al definir una regla una sola vez en un archivo compartido de Lean, los desarrolladores pueden demostrar que la aplicación del navegador nunca enviará una solicitud inválida y que el servidor solo procesará solicitudes que satisfagan esa misma regla. Esto elimina una clase común de errores donde el frontend y el backend discrepan en la lógica de validación. Sin embargo, el sistema tiene límites definidos: mientras que la lógica de la aplicación está verificada formalmente, el entorno de ejecución de JavaScript subyacente, la ejecución de la base de datos SQL y la capa de serialización JSON permanecen fuera del alcance de las pruebas formales. Esto significa que el sistema garantiza la corrección de la lógica interna de la aplicación en lugar de la fiabilidad absoluta de toda la infraestructura de la pila tecnológica.