Lean 4 es un lenguaje de programación funcional que comparte linaje con Haskell y OCaml. Aunque es conocido principalmente como un asistente de pruebas —una herramienta utilizada para verificar matemáticamente la corrección del software—, recientemente ha evolucionado hacia un entorno viable para el desarrollo de aplicaciones de propósito general. La biblioteca estándar del lenguaje ahora incluye un servidor HTTP, y un ecosistema creciente de librerías impulsadas por la comunidad proporciona la infraestructura necesaria para aplicaciones web modernas, incluyendo controladores para PostgreSQL, criptografía y renderizado de HTML.
Para poner a prueba estas capacidades, un desarrollador construyó 'RealWorld', una conocida aplicación de referencia (un clon de Medium) utilizada para evaluar implementaciones full-stack. El proyecto utiliza varios componentes clave: `Std.Http` para el manejo de conexiones de bajo nivel, `lean-routing` para definir rutas de API con parámetros tipados y `leanpostgres` para la interacción con la base de datos. Una elección arquitectónica notable fue el uso de `lean-html` para renderizar páginas como funciones ordinarias de Lean en lugar de utilizar plantillas tradicionales. Para la interactividad del frontend, el proyecto empleó `datastar-lean`, un SDK para Datastar que permite al servidor actualizar la página dinámicamente con pasos mínimos de construcción en el frontend. La implementación del backend resultante fue notablemente concisa, sumando un total de 1,033 líneas de código, una cifra menor que varias implementaciones comunes en TypeScript, Go y C#.
El desarrollador utilizó el proyecto RealWorld para demostrar la capacidad de Lean 4 para manejar requisitos full-stack.
Si bien el proyecto demuestra que Lean 4 puede manejar requisitos full-stack, también resalta compensaciones específicas con respecto a la preparación para producción y la verificación formal. El servidor HTTP actual de Lean tiene limitaciones de rendimiento conocidas, y el rápido ciclo de lanzamientos del lenguaje puede romper dependencias ocasionalmente. Además, aunque Lean permite la 'corrección por construcción' —donde el código se deriva de una especificación formal y cada paso está matemáticamente demostrado—, el desarrollador señaló que la especificación de RealWorld solo era parcialmente formal. Por ejemplo, aunque la aplicación puede demostrar que un 'slug' de URL está bien formado porque se incluye con una prueba matemática de su validez, el comportamiento más amplio de la aplicación todavía depende de pruebas tradicionales. El proyecto sugiere que, si bien Lean 4 ofrece un camino hacia un código verificado de alta calidad, actualmente requiere un equilibrio entre las pruebas formales para la lógica crítica y las pruebas estándar para la funcionalidad general.