‹ BackHN Continuity

Thread

What TLA+ can and can't check

243 points · 51 comments · b-man

  1. adamddev1 · · focus · HN ↗
    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.
    1. nonethewiser · · focus · HN ↗
      I wonder if asking an LLM to model their implementation in TLA+ first would improve their implementations.
      1. senderista · · focus · HN ↗
        A TLA+ spec defines both a model and properties (global invariants). How do you know that the properties the LLM specifies are the ones you care about?
        1. nonethewiser · · focus · HN ↗
          My question is concerned with improving quality of AI implementations. Its plainly true, uninteresting, and beside the point to observe that AI cannot read minds.
Open on Hacker News to reply ↗

Unofficial Hacker News client; not affiliated with Y Combinator.