Birbla

Join the discussion

Write your take first — we'll ask for email only when you're ready to publish.

Sign in
  • Hacker News
  • Gotta love TLA+

    I wonder if anyone has worked on porting it to Lean and making tactics for it

    by vatsachak
  • 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.

    by another_twist
  • 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

    by uptodatenews
  • 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.
    by romaaeterna
  • 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).
    by mempko
  • 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
    by letFunny
  • "to prevent multiple from" seems to be missing a word.
    by stevekemp
  • 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?
    by buggymcbugfix
  • 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?
    by sennalen
  • 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

    by hackingonempty
  • 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. -_-

    by mike_hock