4 ms·

> An API you rely on changes, is deprecated, etc Formal verification will eventually lead to good, stable API design. > Users use something in unexpected ways

by est 10mo ago

> An API you rely on changes, is deprecated, etc Formal verification will eventually lead to good, stable API design. > Users use something in unexpected ways > Complex behavior between interconnected systems It happens when there's no formal verification during the design stage. Formal verification literally means cover 100% state changes and for every possible input/output, every execution branch should be tested.

Joker_vD 10mo 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.
- est 10mo ago
  > 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.
  - Joker_vD 10mo ago
    > 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".
    - est 10mo ago
      > 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)
      - Joker_vD 10mo ago
        > 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. This is literally a dumb light switch. If you have trouble proving that, starting from lights off, flicking a simple switch twice will still keep lights off then, well, I have bad news to tell you about the feasibility of using the formal methods for anything more complex than a dumb light switch. Because the rest of the world is a very complex and stateful place. > (which itself is a state machine of some kind) Yes? That's pretty much the raison d'être of the formal methods: for anything pure and immutable, normal intuition is usually more than enough; it's tracking the paths through enormous configuration spaces that our intuition has problem with. If the formal methods can't help with that with comparable amount of effort, then they are just not worth it.
  - onion2k 10mo ago
    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.
  - wombatpm 10mo ago
    Isn’t this where the Eiffel design by contract people speak up about code reuse?
ehnto 10mo ago
100% of state changes in business software is unknowable on a long horizon, and relies on thoroughly understanding business logic that is often fuzzy, not discrete and certain.
- est 10mo ago
  Formal verification does not gurantee business logic works as everybody expected, nor its future proof, however, it does provide a workable path towards: Things can only happen if only you allow it to happen. It other words, your software may come to a stage where it's no longer applicable, but it never crashes. Formal verification had little adoption only because it costs 23x of your original code with "PhD-level training"
  - bongodongobob 10mo ago
    The reason it doesn't work is businesses change faster than you can model every detail AND keep it all up to date. Unless you have something tying your model directly to every business decision and transaction that happens, your model will never be accurate. And if we're talking about formal verification, that makes it useless.
Almondsetat 10mo ago
Formal verification has nothing to do with the quality of the API. Given the spec, formal verification can tell you if your implementation follows the spec. It cannot tell you if the spec if good
- jeffreygoesto 10mo ago
  That is one problem of many solved, isn't that good? That the spec solves the problem is called validation in my domain and treated explicitly with different methods. We use formal validation to check for invariants, but also "it must return a value xor an error, but never just hang".
- dhruv3006 10mo ago
  Thats something I agree with. I am right now working on an offline api client: https://voiden.md/ https://voiden.md/. I wonder if this can be a feature.
- est 10mo ago
  > It cannot tell you if the spec if good I beg to differ, if a spec is hard to verify, then it's a bad sign.
  - Joker_vD 10mo ago
    All non-trivial specs, like the one for seL4, are hard to verify. Lots of that complexity comes from interacting with the rest of the world which is a huge shared mutable global state you can't afford to ignore. Of course, you can declare that the world itself is inherently sinful and imperfect, and is not ready for your beautiful theories but seriously.
    - jessoteric 10mo ago
      > Of course, you can declare that the world itself is inherently sinful and imperfect, and is not ready for your beautiful theories i see we are both familiar with haskellers (friendly joke!)
  - 10mo ago

by est 10mo ago

Joker_vD 10mo 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.

est 10mo ago
> 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.
- Joker_vD 10mo ago
  > 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".
  - est 10mo ago
    > 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)
    - Joker_vD 10mo ago
      > 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. This is literally a dumb light switch. If you have trouble proving that, starting from lights off, flicking a simple switch twice will still keep lights off then, well, I have bad news to tell you about the feasibility of using the formal methods for anything more complex than a dumb light switch. Because the rest of the world is a very complex and stateful place. > (which itself is a state machine of some kind) Yes? That's pretty much the raison d'être of the formal methods: for anything pure and immutable, normal intuition is usually more than enough; it's tracking the paths through enormous configuration spaces that our intuition has problem with. If the formal methods can't help with that with comparable amount of effort, then they are just not worth it.
- onion2k 10mo ago
  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.
- wombatpm 10mo ago
  Isn’t this where the Eiffel design by contract people speak up about code reuse?

ehnto 10mo ago

100% of state changes in business software is unknowable on a long horizon, and relies on thoroughly understanding business logic that is often fuzzy, not discrete and certain.

est 10mo ago
Formal verification does not gurantee business logic works as everybody expected, nor its future proof, however, it does provide a workable path towards: Things can only happen if only you allow it to happen. It other words, your software may come to a stage where it's no longer applicable, but it never crashes. Formal verification had little adoption only because it costs 23x of your original code with "PhD-level training"
- bongodongobob 10mo ago
  The reason it doesn't work is businesses change faster than you can model every detail AND keep it all up to date. Unless you have something tying your model directly to every business decision and transaction that happens, your model will never be accurate. And if we're talking about formal verification, that makes it useless.

Almondsetat 10mo ago

Formal verification has nothing to do with the quality of the API. Given the spec, formal verification can tell you if your implementation follows the spec. It cannot tell you if the spec if good

jeffreygoesto 10mo ago
That is one problem of many solved, isn't that good? That the spec solves the problem is called validation in my domain and treated explicitly with different methods. We use formal validation to check for invariants, but also "it must return a value xor an error, but never just hang".
dhruv3006 10mo ago
Thats something I agree with. I am right now working on an offline api client: https://voiden.md/ https://voiden.md/. I wonder if this can be a feature.
est 10mo ago
> It cannot tell you if the spec if good I beg to differ, if a spec is hard to verify, then it's a bad sign.
- Joker_vD 10mo ago
  All non-trivial specs, like the one for seL4, are hard to verify. Lots of that complexity comes from interacting with the rest of the world which is a huge shared mutable global state you can't afford to ignore. Of course, you can declare that the world itself is inherently sinful and imperfect, and is not ready for your beautiful theories but seriously.
  - jessoteric 10mo ago
    > Of course, you can declare that the world itself is inherently sinful and imperfect, and is not ready for your beautiful theories i see we are both familiar with haskellers (friendly joke!)
- 10mo ago