alt Hacker NewsParallel programming is a great application for LLM correctness proofs in Lean.
You can't unit test your way out, but if you care about the code's correctness, today there's a way.
Replies
6gvONxR4sf7o • today at 9:15 PM
My experience has been the opposite. If lean had linear types (or separation types), it would be, but as it is, Lean's just a little bit too focused on talking about results to tidily talk about how those results are computed.
tintor • today at 7:40 PM
Mix of different types of tests helps.
Best examples are SQLite and Jepsen test suites for dbms engines.
As I found out recently, there's a lighter option: model checkers like Spin. You describe your synchronization logic in a small modeling language (Promela), and Spin tries every possible interleaving of that model.