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 yo

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.