Harsh Gupta on X: "LeanDB: A strongly typed SQL Frontend " / X

LeanDB: A strongly typed SQL Frontend

At Theoric Labs we believe agentic AI combined with Formal methods can “solve” software. Essentially, we believe software will be fast, and bug free. LeanDB is an experiment in applying part of this idea to databases: describe data and its properties in Lean, while using SQL databases for storage and querying. A Primer on Types in Lean Types are powerful because they allow us to check properties before the code is run. A function expecting a number should not accidentally receive a string. Lean takes this much further. We can express properties as propositions, construct proofs of those…

saved by

• Devin Plumb

related reading

• Building data-centric apps with a reactive relational databaseriffle.systems
• Build Your Own Databasenan.fyi
• A Lean Syntax Primer — overreactedoverreacted.io
• Everything I know about good system designseangoedecke.com
• Lean (proof assistant) - Wikipediaen.wikipedia.org
• Lean Programming Languagelean-lang.org
• A shallow dive into formal verificationvitalik.eth.limo
• Hōrōshi バガボンド (@KatanaLarp) on Xx.com
• On the Unreasonable Effectiveness of Property-Based Testing for Validating Formal Specifications | Proofs and Intuitionsproofsandintuitions.net
• 4. Sets and Functions - Mathematics in Lean v4.19.0 documentationleanprover-community.github.io
• Lean Software Scaling Laws · Gwern.netgwern.net
• Patterns for Building LLM-based Systems & Productseugeneyan.com