infrastructure as code, in Lean 4.

Terraform-style declarative infrastructure, written in the Lean programming language and proof assistant instead of a bespoke DSL. Target and observed cloud state are dependently-typed Lean values, so an unrealisable target is a compile error rather than a failed apply.

A dangling reference, a region a cloud is not in, an instance size that does not exist, a plaintext password in a committed file — none of these get as far as a plan.

• infra @ GitHub.

Related contents:

• Terraform in Lean 4: If It Compiles, It Will Likely Deploy @ NGrislain.