I’ve been building lean-pq, a PostgreSQL connector for Lean 4. While Lean is primarily known for theorem proving, I believe its dependent-types and formal verification features make it the ideal target for AI Agents to generate provably correct code [0]. Lean-pq uses FFI to bind to libpq, but leverages Lean’s type system to move database errors from runtime to compile-time: - Compile-time SQL Validation: Uses Lean’s macro system to check SQL strings against your schema during the build. Misspelled columns or type mismatches cause a build failure. - Monadic Permission Tracking: An effect-tracking monad distinguishes between Read-Only and Read-Write operations. You can statically guarantee a function won't modify the DB: def getUser (id : Int) : DB .ReadOnly User. - Zero-Overhead FFI: Battle-tested libpq performance with Lean 4 ergonomics. The goal is to eliminate runtime surprises—syntax errors, permission violations, and null-mismatches—at the compilation phase. I’d love to hear feedback from anyone exploring Lean 4 for systems programming. Project: https://github.com/typednotes/lean-pq [0] https://ngrislain.github.io/projects/2026-3-12-dont-vibe--pr... |