Lean 4 is a functional programming language that shares lineage with Haskell and OCaml. While it is primarily known as a proof assistant—a tool used to mathematically verify the correctness of software—it has recently evolved into a viable environment for general-purpose application development. The language's standard library now includes an HTTP server, and a growing ecosystem of community-driven libraries provides the necessary infrastructure for modern web applications, including PostgreSQL drivers, cryptography, and HTML rendering.
To test these capabilities, a developer built 'RealWorld,' a well-known reference application (a Medium clone) used to benchmark full-stack implementations. The project utilizes several key components: `Std.Http` for low-level connection handling, `lean-routing` for defining API routes with typed parameters, and `leanpostgres` for database interaction. A notable architectural choice was the use of `lean-html` to render pages as ordinary Lean functions rather than using traditional templates. For frontend interactivity, the project employed `datastar-lean`, an SDK for Datastar, which allows the server to update the page dynamically with minimal frontend build steps. The resulting backend implementation was notably concise, totaling 1,033 lines of code—shorter than several common implementations in TypeScript, Go, and C#.
The developer used the RealWorld project to demonstrate Lean 4's ability to handle full-stack requirements.
While the project proves that Lean 4 can handle full-stack requirements, it highlights specific trade-offs regarding production readiness and formal verification. The current Lean HTTP server has known performance limitations, and the rapid release cycle of the language can occasionally break dependencies. Furthermore, while Lean allows for 'correctness by construction'—where code is derived from a formal specification and every step is mathematically proven—the developer noted that the RealWorld specification was only partially formal. For example, while the app can prove that a URL 'slug' is well-formed because it is bundled with a mathematical proof of its validity, the broader application behavior still relies on traditional testing. The project suggests that while Lean 4 offers a path toward high-quality, verified code, it currently requires a balance between formal proofs for critical logic and standard testing for general functionality.