Lean 4 for Software Engineers

Valentin Erokhin

leangineer.com

Abstract

Lean is not just for mathematicians anymore. You can use it to build real software, today. Lean is a compiled functional language that happens to also be a theorem prover. Most of what's written about it is about the proving part. This site is about the programming part: libraries, tools, and how to actually ship things with them. No category theory required.

1The directory

Awesome Lean collects 367 libraries, tools and projects for building software in Lean, in 27 sections: web servers, databases, FFI, parsers, and more. It's searchable, and it's generated from the awesome-lean list, so a PR there shows up here too.

Browse the directory

2Guides

Hands-on guides: web apps, FFI, and Lean for people coming from Rust, Haskell or TypeScript. Every code sample here gets compiled, so if it's on the site, it works.

sorry These aren't written yet.

3How this site is built

Theorem 1 (Written in Lean). Every page on this site is a typed HTML value produced by a Lean program.

Proof. Yes, really. Pages are built with lean-html, so if I put a <div> inside a <p>, it doesn't compile. The directory is parsed from the awesome-lean readme with a Markdown parser that is proved to produce well-formed HTML. Search streams results from the server with Datastar, so there's no frontend build step and no client-side state to manage. The routes are in Figure 1; the infoview agrees.

Main.lean
-- the routes this page was served from
route_table Site
  [ home     := "/",
    awesome  := "/awesome",
    category := "/awesome/:slug:String" ]

def hero : Node .flow :=
  h1 [ "Lean 4 for Software Engineers" ]

theorem site_is_written_in_lean : True := by
  trivial
Lean Infoview

▼ Main.lean:10:2

No goals

✓ Goals accomplished

Figure 1. The route table this page was served from, and Lean's verdict.

∎

I think that's a pretty good demo of what Lean can do outside of math. The code is open source, if you want to see how it's done.

4About the author

Hi, I'm Valentin. I made Lightbug, the first HTTP framework for Mojo, and datastar-lean. I'm collecting what I learn about writing real software in Lean here. Hit me up on Bluesky or on the Lean Zulip if you have questions or ideas.