Hunting a 16-year-old SQLite WAL bug with TLA+
1–10 of 37 posts
Re: Hunting a 16-year-old SQLite WAL bug with TLA+
#2[flagged]
Re: Hunting a 16-year-old SQLite WAL bug with TLA+
#3TLA+ = 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.)
Re: Hunting a 16-year-old SQLite WAL bug with TLA+
#4TLA+ = 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.) https://lamport.azurewebsites.net/tla/tla.html
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. -_-
Re: Hunting a 16-year-old SQLite WAL bug with TLA+
#5Gotta love TLA+
I wonder if anyone has worked on porting it to Lean and making tactics for it
Re: Hunting a 16-year-old SQLite WAL bug with TLA+
#6TLA+ = 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.) https://lamport.azurewebsites.net/tla/tla.html
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. -_-
Leslie Lamport is also the original creator of LaTeX.
Re: Hunting a 16-year-old SQLite WAL bug with TLA+
#7Gotta love TLA+ I wonder if anyone has worked on porting it to Lean and making tactics for it
You run into Rices theorem if you try to apply it too heavily.
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
Re: Hunting a 16-year-old SQLite WAL bug with TLA+
#8Author of the article here. I am surprised to see the post was submitted and made it to the front page! Happy to answer any questions
Re: Hunting a 16-year-old SQLite WAL bug with TLA+
#9Author of the article here. I am surprised to see the post was submitted and made it to the front page! Happy to answer any questions
"to prevent multiple from" seems to be missing a word.
Re: Hunting a 16-year-old SQLite WAL bug with TLA+
#10Gotta love TLA+ I wonder if anyone has worked on porting it to Lean and making tactics for it
i am not sure if a lean port is important. TLA+ could do with a bit more TLC (pun intended) with regards its devEx.
Also congratulations to the author, I'll try and reproduce this over the weekend.