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.
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.
What you say reminds me of the "Von Neumann Languages Lack Useful Mathematical Properties" section in John Backus's Turing award paper. One of his criticisms of what we would now call imperative languages is that they make it exceedingly difficult to formally prove facts about a program.
>> 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
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.
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
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.
What you say reminds me of the "Von Neumann Languages Lack Useful Mathematical Properties" section in John Backus's Turing award paper. One of his criticisms of what we would now call imperative languages is that they make it exceedingly difficult to formally prove facts about a program.
https://dl.acm.org/doi/epdf/10.1145/359576.359579
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
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.
Related:
The internet discovers TLA+. Now what?
https://news.ycombinator.com/item?id=49863600