Lean-pq a typesafe PostgreSQL connector for lean

Name: Lean-pq a typesafe PostgreSQL connector for lean
Availability: InStock
Author: ngrislain

by ngrislain·Mar 14, 2026·2 points·1 comment

Visit Project View on HN

AI Analysis

●●SolidBig BrainNiche Gem

Compile-time SQL validation using Lean's type system moves database errors from runtime to build.

Strengths

•Monadic permission tracking distinguishes ReadOnly vs ReadWrite operations in types
•Column references carry proofs that eliminate runtime schema mismatches
•Zero-overhead FFI binding to battle-tested libpq with Lean ergonomics

Weaknesses

•Extremely narrow audience — Lean 4 users who need PostgreSQL are rare
•No Windows support mentioned, and Lean ecosystem is still nascent

Post Description

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...