TLA+ = formal language for modeling software above the code level and hardware above the circuit level by Leslie Lamport (of vector clock and Paxos fame, among other things.)
You’re in a desert walking along in the sand when all of the sudden you look down, and you see a tortoise, it’s crawling toward you. You reach down, you flip the tortoise over on its back. The tortoise lays on its back, its belly baking in the hot sun, beating its legs trying to turn itself over, but it can’t, not without your help. But you’re not helping. Why is that?
I don't like the title. The article actually describes the process of proving that dqlite does not have the same bug as SQLite, using a TLA+ specification. The SQLite bug fix was entirely separate from what is described here.
This is so cool and I wonder how effective it would be using this technique when using LLMs to generate code. Have the llm generate code and a TLA+ model. Use the TLA+ model as the test bed of the code (instead of writing tests in the original language).
13 comments
[ 0.21 ms ] story [ 30.4 ms ] threadhttps://lamport.azurewebsites.net/tla/tla.html
I wonder if anyone has worked on porting it to Lean and making tactics for it