‹ 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. IshKebab · · focus · HN ↗
      How do managers build software?

      The fact is when LLMs get good enough you WILL be able to build software without reading/understanding the code.

      Whether or not you think we are already at that point is kind of an unimportant detail.

      I would say we are quite close, depending on the type of software you are building.

      1. jasomill · · focus · HN ↗
        This is like saying that computers will get fast enough and compilers will be good enough at catching mistakes that you won't need to care about performance or correctness.

        Good luck with that.

        As system complexity continues to increase, tools that are inherently difficult to predict and therefore reason about are unlikely to be the panacea that many today believe them to be.

Open on Hacker News to reply ↗

Unofficial Hacker News client; not affiliated with Y Combinator.