Comment by ibarrajo

4 hours ago

I’ve been vibe coding a lot of Lean this year.

What i found is that it is amazing once you determine and the invariants that are essential to the guarantees you want to keep.

I built my own formally verified workflow engine, it was easy but mostly because i already knew the pitfalls and the foundational pillars of Cadence and Temporal.

Also, it doesnt seem like common knowledge, but you can export libraries that compile to C from lean. With them you do get performant code that that has been verified and easily call them as C bindings from elsewhere.

Lean itself does not have a good IO stack in general but its good enough for small projects.

There is a caveat to exporting libs or native_decide in general. Once you export into C, ABI its now outside of the scope of the Lean kernel which means that bugs can creep in from the compiler itself.

3 comments

ibarrajo

Reply
nylonstrung  3 hours ago

I'd love to hear more about your workflow engine, I think the expressiveness of lean and the type system makes it extremely well suited for stuff like that

I do agree that the lack of IO and libs in lean isn't really a drawback when there's a very clear interop path already

sroerick  1 hour ago

I'd love to know more about your experience on this, generally. What have you been doing in Lean? How have you approached this?