Live data from Hacker News

Hunting a 16-year-old SQLite WAL bug with TLA+

ubuntu.com

31–37 of 37 posts

Re: Hunting a 16-year-old SQLite WAL bug with TLA+

#31

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.) 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. -_-

If the LaTeX-like syntax worries you, several projects aimed at providing PL-like syntaxes for TLA+. They vary by their degree of how much of the logic they throw away. I am not going to advertise these projects here, but you would find them on GitHub search by typing the tags like "#tlaplus #language", "#tlaplus #library", and "#tlaplus #pluscal".

Re: Hunting a 16-year-old SQLite WAL bug with TLA+

#32

Earlier quoted context omitted.

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. -_-

If the LaTeX-like syntax worries you, several projects aimed at providing PL-like syntaxes for TLA+. They vary by their degree of how much of the logic they throw away. I am not going to advertise these projects here, but you would find them on GitHub search by typing the tags like "#tlaplus #language", "#tlaplus #library", and "#tlaplus #pluscal".

No, I just find the inconsistent syntax annoying, but it turns out most things have alternative Latex-style spellings. I just went by their examples.

Re: Hunting a 16-year-old SQLite WAL bug with TLA+

#34
post #8

Author 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

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 feel like I'm ignorant of some classical fable here.

Is this an allusion?

Re: Hunting a 16-year-old SQLite WAL bug with TLA+

#35

Earlier quoted context omitted.

We found it at Tailscale and bought an enterprise support contract from SQLite to debug it for us. Worth every penny. We should probably blog about it.

What mission critical purpose does sqlite provide at Tailscale exactly? Why use it at all?

Quite a bit, it seems: https://tailscale.com/blog/database-for-2022

Re: Hunting a 16-year-old SQLite WAL bug with TLA+

#36

Earlier quoted context omitted.

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 feel like I'm ignorant of some classical fable here. Is this an allusion?

It's a Blade Runner reference [1].

[1] https://bladerunner.fandom.com/wiki/Voight-Kampff_test

Post reply on HN