b-man · 33 points · 4 comments · 3 時間前 · Open original
Comments
4 preview comments · loading full thread
Log in to use comments
Log in to h4cker, then connect Hacker News to publish comments.
SOsourdecor32 分前
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
RRrrook33 分前
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.
CHChrisArchitect16 分前
Related:
The internet discovers TLA+. Now what?
https://news.ycombinator.com/item?id=49863600
ADadamddev11 時間前
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.
Comments
4 preview comments · loading full threadLog in to h4cker, then connect Hacker News to publish comments.
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.
Related: The internet discovers TLA+. Now what? https://news.ycombinator.com/item?id=49863600
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.