> leverages Lean’s type system to move database errors from runtime to compile-time

Really cool.

Found your post by searching for "lean" via algolia. The language grabbed my attention when Mistral trained a model for it. Care to share your experience with it? Anything you wish you knew when you were getting started?

Edit: reading through your blog post, didn't notice it at first.