← Back to context

Comment by Joker_vD

8 days ago

> Formal verification will eventually lead to good, stable API design.

Why? Has it ever happened like this? Because to me it would seem that if the system verified to work, then it works no matter how API is shaped, so there is no incentive to change it to something better.

> if the system verified to work, then it works no matter how API is shaped

That's the case for one-off integrations, but the messy part always comes when system goal changes

Let's say formal verification could help to avoid some anti-patterns.

  • > Let's say formal verification could help to avoid some anti-patterns.

    I'd still like to hear about the actual mechanism of this happening. Because I personally find it much easier to believe that the moment keeping the formal verification up to date becomes untenable for whatever reason (specs changing too fast, external APIs to use are too baroque, etc) people would rather say "okay, guess we ditch the formal verification and just keep maintaining the integration tests" instead of "let's change everything about the external world so we could keep our methodology".

    • > I'd still like to hear about the actual mechanism of this happening

      I am not an expert on this, but the worst API I've seen is those with hidden states.

      e.g. .toggle() API. Call it old number of times, it goes to one state, call it even number of times, it goes back.

      And there's call A before you call B types of APIs, the client has to keep a strict call order (which itself is a state machine of some kind)

      1 reply →

  • At that point you create an entirely new API, fully versioned, and backwardly compatible (if you want it to be). The point the article is making is that AI, in theory, entirely removes the person from the coding process so there's no longer any need to maintain software. You can just make the part you're changing from scratch every time because the cost of writing bug-free code (effectively) goes to zero.

    The theory is entirely correct. If a machine can write provably perfect code there is absolutely no reason to have people write code. The problem is that the 'If' is so big it can be seen from space.

  • Isn’t this where the Eiffel design by contract people speak up about code reuse?