Comment by thomasahle
4 hours ago
Parallel 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.
4 hours ago
Parallel 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.
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.
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.
Mix of different types of tests helps.
Best examples are SQLite and Jepsen test suites for dbms engines.
https://jepsen.io/