DigiNews

Summary

LeanDB proposes a strongly typed SQL frontend where schema, queries, and migrations are represented as types in Lean 4. The compiler enforces correctness across these dimensions, enabling compile-time validation and safer data handling. A first cut LeanDB v0.1 is available on GitHub, with design goals including compatibility with existing SQL databases and a plan to integrate with compute.cx.