> 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 lang

> 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.