Like Terraform, but in Lean 4

Where the mistakes are caught

The loop itself is Terraform's: observe, diff, reconcile. What differs is where the mistakes are caught. Working that out turned out, to my mild surprise, to be most of the design effort, and the repository keeps the answer in a table:

Two different things happen in those compile-time rows. In the first four the mistake has no spelling: there is no way to write the broken configuration down, so nothing has to be checked. In the next two you can write it down, and the compiler decides by running a small function over what you wrote. (Lean people call that second kind an elaboration-time check. For the rest of this post it is just compilation.)

The last two rows are the honest half of any "types catch bugs" claim. Compiling is not a promise that the apply will succeed. It is a promise about which failures are still on the table when you get there.

The differences, listed

Before the code, the short version of what this buys over HCL:

The last row is why you should still use Terraform this week. The rest, I think, is worth stealing.

Side by side

fleet webTier in paris where
  resource aws securityGroup "web" as web
    { description := "http and https, ssh from nowhere" }

  resource aws awsInstance "web-1"
    { imageId       := "ami-0123456789abcdef0"
    , instanceType  := InstanceType.of .t3 .nano
    , securityGroup := web }

provider "aws" {
  region = "eu-west-3"
}

resource "aws_security_group" "web" {
  name        = "web"
  description = "http and https, ssh from nowhere"
  region      = "eu-west-3"
}

resource "aws_instance" "web-1" {
  ami                    = "ami-0123456789abcdef0"
  instance_type          = "t3.nano"
  vpc_security_group_ids = [aws_security_group.web.id]
  region                 = "eu-west-3"
}

securityGroup : Field .required o f (K .aws .securityGroup)

Application type mismatch: The argument
  fun securityGroup => Build.awsInstance … securityGroup
has type
  Expr ?m (?m ProviderId.aws Kind.securityGroup) → AwsInstanceSpec …
but is expected to have type
  SpecOf Kind.awsInstance keys.Key Partial (Expr keys.Key)

def InstanceType.of (f : InstanceFamily) (s : InstanceSize)
    (_h : Assert (f.sizes.contains s) := by decide) : InstanceType :=
  ⟨s!"{f.code}.{s.code}"⟩

could not synthesize default value for parameter '_h' using tactics
Tactic `decide` proved that the proposition
  Assert (InstanceFamily.t3.sizes.contains InstanceSize.xlarge32)
is false

#guard Locality.paris.code .aws        = some "eu-west-3"
#guard Locality.paris.code .scaleway   = some "fr-par"
#guard Locality.warsaw.code .aws       = none
#guard Locality.ireland.code .scaleway = none

fleet crossCloud in paris where
  resource aws objectStore "typednotes-assets"
    { versioning := true }

  resource scaleway objectStore "typednotes-assets"
    { versioning := true }

provider "aws" {
  region = "eu-west-3"
}

provider "scaleway" {
  region = "fr-par"
}

resource "aws_s3_bucket" "typednotes-assets" {
  bucket = "typednotes-assets"
  region = "eu-west-3"

  versioning {
    enabled = true
  }
}

resource "scaleway_object_bucket" "typednotes-assets" {
  name   = "typednotes-assets"
  region = "fr-par"

  versioning {
    enabled = true
  }
}

#guard (Finite.elems (α := Locality)).filter (·.covers crossCloud.keys)
     = [.paris, .milan]

inductive SecretSource
  | fromEnv  (varName : String)
  | composed (value   : String)
  deriving DecidableEq, BEq

#guard ¬ ({ name := "leak", valueFrom := .lit (.composed "hunter2") } :
  SecretsSpec composedKeys.Key Partial (Expr composedKeys.Key)).sourceIsSound

#guard ¬ ({ name := "leak", valueFrom := composed (.lit "hunter2") } :
  SecretsSpec composedKeys.Key Partial (Expr composedKeys.Key)).sourceIsSound

Dependencies you do not declare

This is the part I would carry into a real tool first, because it is where the two diverge most, and none of it has to do with catching errors.

Some of what you declare does not exist yet: an endpoint the cloud assigns, a password you generate. Here a declaration can hold a recipe for such a value, and the shorthand looks like ordinary string interpolation:

resource scaleway secrets "db-password" as pw
  { valueFrom := fromEnv "DB_PASSWORD" }

resource scaleway postgres "main" as db
  { masterUsername := "dbadmin", maxCapacity := 4 }

resource scaleway secrets "db-url"
  { valueFrom := composed
      expr!"postgres://dbadmin:{secretValueOf pw}@{endpointOf db}/main" }

The two holes in that string are two arrows in the graph.

Secrets are the obvious case, but they are not the only one: any field can hold such a recipe, and any post-apply value can go in one. secretValueOf and endpointOf are simply the two projections common enough to have names in the library, and each is one line over the general form, which is observedOf and a field:

def privateIpOf {p : ProviderId} (key : K p .awsInstance) : Expr K String :=
  (observedOf key).map (·.privateIp)

An instance's private address does not exist until the instance launches, so a peer list built out of two of them is the connection string again, one kind further out:

fleet cluster in paris where
  resource aws securityGroup "web" as web
    { description := "http and https, ssh from nowhere" }

  resource aws awsInstance "app-1" as app1
    { imageId       := "latest"
    , instanceType  := InstanceType.of .t3 .nano
    , securityGroup := web }

  resource aws awsInstance "app-2" as app2
    { imageId       := "latest"
    , instanceType  := InstanceType.of .t3 .nano
    , securityGroup := web }

  resource aws secrets "cluster-peers"
    { valueFrom := composed expr!"{privateIpOf app1},{privateIpOf app2}" }

Three kinds, two ways of referring to another resource, and one diamond. securityGroup := web is a reference in a field: the group has to exist before either instance, and the type says so. The two holes in the last string are references inside a value: each instance has to exist, and have launched, before the peer list can be written. Nothing distinguishes them to the scheduler, because both report the same edges:

Four resources, four creates, one apply. The order comes from those arrows: nothing in the file says the group goes first, or that both instances are running before the peer list is written. There is no depends_on in the language, because a reference is the dependency, so the graph cannot disagree with the code. Creation is Kahn's algorithm over the edges the references report, and deletion is the same graph transposed, so teardown is the reverse rather than a separate guess. That last part matters here: EC2 refuses to delete a security group an instance still references, and the reversed diamond gets the instances gone first without anyone saying so.

Arbitrary shapes are fine. Here is a fan-out, a fan-in of three with one redundant edge, and a four-deep chain, all in five secrets:

fleet secretGraph in paris where
  provider aws where
    resource secrets "db-base"      as base { valueFrom := fromEnv "DB_PASSWORD" }
    resource secrets "app-a"        as a    { valueFrom := composed expr!"a:{secretValueOf base}" }
    resource secrets "app-b"        as b    { valueFrom := composed expr!"b:{secretValueOf base}" }
    resource secrets "app-combined" as sink { valueFrom := composed
        expr!"{secretValueOf a}|{secretValueOf b}|{secretValueOf base}" }
    resource secrets "app-tail"           { valueFrom := composed expr!"t:{secretValueOf sink}" }

Nothing in it mentions ordering, and the plan comes out sorted:

would CREATE aws/secrets/db-base
would CREATE aws/secrets/app-a
would CREATE aws/secrets/app-b
would CREATE aws/secrets/app-combined
would CREATE aws/secrets/app-tail

Now write the same fleet in HCL. It has to give up on every one of the five:

resource secrets "db-base" as base
  { valueFrom := fromEnv "DB_PASSWORD" }

resource secrets "app-a" as a
  { valueFrom := composed
      expr!"a:{secretValueOf base}" }

resource secrets "app-tail"
  { valueFrom := composed
      expr!"t:{secretValueOf sink}" }

resource "aws_secretsmanager_secret" "db-base" {
  name   = "db-base"
  # TODO value: a secret's value is never in the
  # declaration; wire it up in Terraform yourself
  region = "eu-west-3"
}

resource "aws_secretsmanager_secret" "app-a" {
  name   = "app-a"
  # TODO value: a secret's value is never in the
  # declaration; wire it up in Terraform yourself
  region = "eu-west-3"
}

resource "aws_secretsmanager_secret" "app-tail" {
  name   = "app-tail"
  # TODO value: a secret's value is never in the
  # declaration; wire it up in Terraform yourself
  region = "eu-west-3"
}

Those # TODO lines are HCL refusing to guess, and I think they are the fairest picture of the gap. The names and the regions translate. The graph does not, because in HCL a secret's value is a second resource wired up by hand, and composing one from three others is yours to assemble and yours to order.

The same holds when a dependency crosses clouds. A Scaleway function reading an AWS bucket, and a function placed in a namespace this fleet also creates, come out ordered:

$ lake exe cross-cloud

would CREATE aws/object-store/typednotes-assets
would CREATE aws/s3-bucket/typednotes-archive
would CREATE scaleway/object-store/typednotes-assets
would CREATE scaleway/scaleway-function-namespace/typednotes
would CREATE scaleway/scaleway-function/reindex

The namespace before the function that lives in it, the bucket before the function that reads it, one apply, two clouds, and the reference is the only thing that says so. HCL gets the same edges when a value flows through an expression, and depends_on is for the rest: the dependency is real, nothing in the code carries it, and you have to remember. Here there is no rest. A reference is the only way to name another resource, so the graph cannot be less complete than the code.

resource "aws_instance" "web" {
  for_each  = toset(aws_subnet.tier[*].id)   # created in this same apply
  subnet_id = each.value
}

inductive Expr (K : ProviderId → Kind → Type) : Type → Type 1 where
  | lit         : α → Expr K α
  | observed    (p : ProviderId) (k : Kind) : K p k → Expr K (ObservedOf k)
  | secretValue (p : ProviderId) : K p .secrets → Expr K String
  | map         : (α → β) → Expr K α → Expr K β
  | ap          : Expr K (α → β) → Expr K α → Expr K β

Why dependent types actually help here

"Dependent types" means types that can mention values. Four separate things follow from that here, and only the first is the one people usually have in mind.

A type can name a value. A region is not a string, it is a region of a particular cloud, and the cloud is in its type: Region .aws and Region .scaleway are different types, so an AWS region cannot reach a Scaleway call. Same for references. Useful, and the least interesting item here.

The compiler will run your own checks. The one with no HCL equivalent, and the whole of it is four lines:

@[reducible] def Assert (b : Bool) : Prop := b = true

Assert b claims that b comes out true. Because a type can mention a value, that claim can be about your configuration, which is what the instance-size and placement checks above are. Anything a program can compute about a configuration can go there: that the dependency graph has no cycles, that you asked for at most twenty servers, that a name uses only the characters the cloud accepts. Without this you write those as a linter, which is a second implementation of what your configuration means, in another language, run at another time, free to disagree with the first. Here the check is an ordinary function next to the data it checks, and the compiler is what runs it.

The error messages are the payoff, and I did not write any of them:

Tactic `decide` proved that the proposition
  Assert (Locality.warsaw.covers keys)
is false

That is the compiler quoting my own check back at me, with my own file substituted into it. The same move covers what HCL leaves to a runbook. Terraform stops managing a resource without destroying it via a removed block; here it is forget scaleway queues "old-queue", and the compiler owns it: forgetting something you still declare does not compile, one fleet's releases cannot be handed to another because the type carries the fleet, and a release cannot be built by hand because the only constructor is the checked one.

One table does three jobs. The table of places maps each place to each cloud's own code. Autocomplete lists the places from it, the compile-time check reads it, and the assertions pin its entries: three consumers reading one source, not three copies of the same list that could quietly diverge. In HCL the equivalent knowledge, which region codes a provider accepts, lives in the provider's Go source, in its documentation, and in your head, and those three disagree often enough to be its own class of bug report.

A half-built resource is not a value. A required field has no default and cannot be left unset, so a half-built resource is not an object with nulls in it. It is a function still waiting for an argument, which is why a missing security group reads as a type mismatch about a function. That is the shift I would keep, and it is not "the type system rejects bad configurations". It is that the set of things you can write can be made close to the set of things you could deploy.

One detail I believe is load-bearing for anyone attempting this: none of it is worth much if a stale table stands in the way, and these tables are snapshots of catalogues that keep growing. Region.raw and InstanceType.raw take a string on trust, so falling behind a provider costs a somewhat conspicuous spelling rather than a wall. Get that wrong, and the first missing region turns the type system into an adversary.

Being fair about it

What the live run in CI actually exercises, and what it leaves out:

Deleting a line is where the two tools are most alike in effect and least alike in machinery. Both need to answer one question: after its line is gone, is this resource mine to destroy or a stranger's to leave alone? Terraform answers from state, a remote file listing what it created. Here the answer comes from a marker tag written onto everything the tool creates, checked against an account boundary and a human-maintained exclusion list — ownership as a property of the resource, not an entry in a file on my laptop.

A local, gitignored ledger caches that answer, one row per resource, so an apply does not have to ask the cloud what it owns every time it runs. Committing that cache instead, which I tried first, was the actual mistake: a row appears because a resource was created, an event on whichever machine ran the apply, not a statement of intent. Writing that back to a shared branch needs push permissions, races with concurrent merges, and a loop unless carefully guarded. Terraform keeps state remote for the same reason, and I rediscovered it the slow way. Losing the cache costs nothing now but a moment's wait — a discover command rebuilds it by reading the marker straight back off the account.

The direction of the check is what I would defend regardless of storage. It is a list of what to include, and the two directions fail very differently: losing it means something keeps running untracked and costs money until someone notices, while a false include on a list of what to avoid means deleting a stranger's database. The marker only ever grants; the exclusion list only ever takes away.

None of that is what types are for. Ownership is a question about what happened on some past machine, not about what is well-formed on this one — and some things stay at runtime whatever you do: whether a bucket name is globally unique, whether your quota covers the instance, whether the cloud has caught up with itself.

The scale gap is the real answer to "should you use this". Fourteen resource kinds against Terraform's thousands, three clouds instead of hundreds of providers. No module registry, no state locking, no team workflow. If you need to ship infrastructure this week, use Terraform.

What two weekends bought

On the original question, iterating faster: yes, and not in the way I expected. The compile-time checks are satisfying but they fire once each. What actually changed the loop is that a broken configuration usually has no spelling, so the file I am editing is either wrong in a way the editor underlines immediately or right in a way that reaches an apply. There is very little middle ground where something plausible sits waiting to fail after the fourth resource. That middle ground is where Terraform time goes.

It is also what made the AI collaboration work. Two weekends and 18,000 lines were not typed by me, mostly. Most of it was written in a loop where an agent proposes and the compiler judges, and the reason that loop converges is that the types carry the intent. When I say a reference must be a security group in this fleet, that is not a comment an agent may quietly drift from — it is a constraint the next suggestion must satisfy. The tighter the types, the less review the code needs, which is the opposite of what type systems are usually sold as costing.

What I would carry into a real tool is narrower than the tool. Make the desired state a value whose type is narrow enough that undeployable configurations are hard to write. Let references be typed indices into the declaration, so ordering is derived and depends_on never exists. Let the compiler run your own checks rather than maintaining a linter that can disagree with them. And give every lookup table a deliberately ugly way out. Almost all of the remaining 18,000 lines are HTTP clients — and, predictably enough, that is where the bugs live.

The code is at github.com/typednotes/infra, and docs/coverage.md is the honest account of how far it has been run, including the embarrassing parts.