Thread

What TLA+ can and can't check

243 points · 51 comments · b-man

westurner · 1790791275 · focus · HN ↗
From "How did software get so reliable without proof? (1996) [pdf]" (2024) <a href="https://news.ycombinator.com/item?id=42425617">https://news.ycombinator.com/item?id=42425617 :
> From "The Future of TLA+ [pdf]" (2024) <a href="https://news.ycombinator.com/item?id=41385141">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
1. grohan · 1790863677 · focus · HN ↗
  I quite enjoyed Tony Hoare's essay - thanks for sharing. A lot of what he wrote has stood the test of time!
  1. westurner · 1790912027 · focus · HN ↗
    Re: Hoare logic; Precondition, Command, Postcondition: <a href="https://news.ycombinator.com/item?id=47335703">https://news.ycombinator.com/item?id=47335703
    "Three ways formally verified code can go wrong in practice" re: Hoare logic and DbC Design-by-Contract patterns: <a href="https://news.ycombinator.com/item?id=45562815">https://news.ycombinator.com/item?id=45562815

Unofficial Hacker News client; not affiliated with Y Combinator.