GoKawiilLeanDB project brings compile-time type checking to SQL schemas and queries
A developer has published an early version of LeanDB, an experimental SQL frontend built in the Lean 4 programming language that lets database schemas, queries and migrations be expressed as strongly typed constructs the compiler can verify. The post walks through Lean 4's dependent type system, showing how types can carry provable conditions—like an age under 150 or a validated email—so invalid data is rejected before code ever runs. It's presented as a first version, with the author inviting feedback on where the design falls short.