SQL in Lean?

Stream: general

[Andrew Quinn]

I've been poking around the edges of the Lean 4 community tonight, as a theorem prover that doubles as a general purpose programming language is very interesting indeed. To my surprise I haven't found much in the way of production grade SQL libraries yet. I am wondering why that is, whether there are blockers I as a non-mathematician (but mathematically inclined, did my minor in it, etc) am missing here.

[Snir Broshi]

#general > SQLite bindings for Lean
(or do you mean pure Lean implementations, including proofs?)

[Andrew Quinn]

Thanks for the link! And, no, that would be killer but I don't think I'd be that lucky.

[Kim Morrison]

@Andrew Quinn, please see https://github.com/leanprover/leansqlite