HN

Comments (25)

• sourdecor
  I discovered Quint[0] due to this comment[1] on HN. Quint is "an executable specification language [which works in JavaScript] with delightful tooling based on the temporal logic of actions (TLA)". I think it is awesome and anybody interested in TLA+ should check it out.[0]: https://github.com/quint-co/quint[1]: https://news.ycombinator.com/item?id=49865720
• Menu

  singron
  I love this. This is great to read if you are trying to use TLA+ for something.In a different vein, another thing TLA+ isn't great at is modeling atomics and in particular weak-memory semantics or anything that's not sequentially consistent. If you translate your algorithm to pcal, it will run as if it was sequentially consistent. If you need to model non-sequential-consistency, then that needs to be spelled out with explicit logic to TLA+, which is probably too complicated and error-prone to do by hand. The C/C++/Rust memory models permit a lot of wacky stuff. I imagine you need to add read caches and writeback buffers for each variable with cache-flushing instructions at appropriate points, but maybe there is a more elegant way to do it.If you use rust, miri and loom both have analyzers that can check some non-sequentially-consistent behavior (and loom doesn't actually implement sequential-consistency at all).
• Menu

  adamddev1
  Great write-up. People keep saying "we can just write tests" or more recently "we can use formal verification," thinking these are sufficient safeguards we can use and then relegate all the implementation to LLMs. But the fact is that probabilistic guessing machines can't save them. People can't escape the need to actually understand the things they are building.
• Menu

  IshKebab
  IMO TLA+ is not very good. It has super weird syntax, and a whole separate DSL (PlusCal) to give it workable syntax for programs. You can really tell it was created by the same mind as LaTeX.What is the Typst of formal modeling?Another issue is that you end up with a formal model that passes, but then you have still have to convert that to a real language by hand and not make any mistakes.
• Menu

  rrook
  i think part of this is a shortcoming of our programming languages. generally, languages allow for the expression of partial graphs, which makes the verification problem technically challenging. my take is that a language that only exposes closed-graph semantics could help bridge the gap between the model and the implementation, even if not absolute.
• ChrisArchitect
  Related:The internet discovers TLA+. Now what?https://news.ycombinator.com/item?id=49863600
• westurner
  From "How did software get so reliable without proof? (1996) [pdf]" (2024) https://news.ycombinator.com/item?id=42425617 :> From "The Future of TLA+ [pdf]" (2024) https://news.ycombinator.com/item?id=41385141 :>> Formal methods including TLA+ also can't/don't prevent or can only workaround side channels in hardware and firmware that is not verified. But that's a different layer.>> Things formal methods shouldn't be expected to find: Floating point arithmetic non-associativity, side-channels
• Menu

  lou1306
  Uhm, I can see the desire to simplify, but the passage about "reachability" sounds odd.Sure, TLA+ lets you verify whether P is true in every state of every behavior by checking []P. But a _counterexample_ to that property, if it exist, is _some_ state in _some_ behaviour where P is false. Thus, if your model checker proves []P false, you have indirectly proven E<>!P (where the initial E means exactly "for some behaviour").Going back to the example, "proving that a game is winnable" should be achievable by model checking the invariant "the game is never winnable" and failing. Or am I missing something here?
• kylegalbraith
  [dead]