Terraform in Lean 4: If It Compiles, It Will Likely Deploy

I spent two weekends building infra, a Terraform-style infrastructure-as-code tool in Lean 4. It spans three clouds, 14 resource kinds, about 15,000 lines of Lean, and 107 commits. It is not production software. But the point of the exercise isn’t polish anyway. It’s what a real type system can do to infrastructure code when the language is allowed to care about the shape of the deployment.

The basic loop is familiar: declare what you want, inspect what the cloud already has, reconcile the gap. The difference is where the bad news shows up. In this system, a reference to something that isn’t there, a missing required field, using a service a cloud doesn’t offer, or asking for a region a cloud isn’t in can all fail at compile time. A bucket name somebody already took, or the usual mess of quotas, capacity, and eventual consistency, still show up at runtime. That boundary matters. It changes what “types catch bugs” actually means.

The nicest part is that some mistakes don’t even have a spelling. If a resource needs a security group, leaving it out doesn’t become a late validation error; the thing just won’t compile. If an instance size doesn’t exist, Lean can compute that from the family and size you picked and reject the impossible combination. The same trick works for regions and cloud-local names. Locality.paris maps to AWS and Scaleway, while Locality.warsaw is absent from AWS, so an AWS resource in Warsaw is a compile error and a Scaleway one may not be. The compiler is not checking strings. It is checking the actual combinations.

That same pattern reaches secrets and dependencies. A secret can only come from a declared source, not from a stray literal dressed up to look legitimate. And there is no way to branch on an unknown value to decide how many resources to create, which means the old Terraform problem of “can’t plan this until you’ve already applied part of it” gets pushed out of the language entirely. You can still feed unknown values into fields. You just can’t use them to decide how many things exist.

This is the interesting part of the project: the checks aren’t bolted on next to the config. They are the config. The compiler runs the rules, and the rules are written in the same file as the resources they describe. That’s why the error messages are unusually blunt, and why the system can keep a table of valid regions, sizes, and places without asking a human to maintain three copies and hope they drift in sync less often than usual.