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.
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.)
So there's \in, \subseteq and probably many others that are written just like in Latex. Notably \cap and \cup were also copied from Latex, which describe the shape of the symbol instead of its meaning. But not \to, \mapsto, \Vee and \Wedge, they're written as ASCII art ->, |->, \/ and /\.
Then there's SUBSET, which means power set ... yeah. -_-
Thanks for the nice article. The SQLite docs that explain this bug are emphatic about how utterly rare, even irreproducible it is. How, then, was it found, one wonders?
My guess is that they noticed something was not quite right when inspecting the code and then tested their hypothesis manually to see if it was actually a real bug.
Something similar happened to me when I was working on some code that should clear the state and, by inspection, I noticed some field was not properly cleared under specific circumstances. Then I tested the hypothesis and indeed found a bug. Sometimes intuition and guessing is what it takes.
For local only high level modelling. Its not a full tie into the actual model checker, but its meant to serve as a first step into system modelling for state machine modelling for beginners
https://lamport.azurewebsites.net/tla/tla.html
Then there's SUBSET, which means power set ... yeah. -_-
Something similar happened to me when I was working on some code that should clear the state and, by inspection, I noticed some field was not properly cleared under specific circumstances. Then I tested the hypothesis and indeed found a bug. Sometimes intuition and guessing is what it takes.
I wonder if anyone has worked on porting it to Lean and making tactics for it
I made https://github.com/RCSnyder/tlaplus-process-studio
https://tlaplus-process-studio.com/
For local only high level modelling. Its not a full tie into the actual model checker, but its meant to serve as a first step into system modelling for state machine modelling for beginners
Also congratulations to the author, I'll try and reproduce this over the weekend.