7 ms·

Why should it save labor. What it does is guarantee correctness which is like the holy grail for programmers. If you know shit's correct you can just assume stu

Why should it save labor. What it does is guarantee correctness which is like the holy grail for programmers. If you know shit's correct you can just assume stuff and it will actually work on the first try. You don't even need to write tests for it.

twinkjock 2y ago
This is why connecting formal verification to an infinite (possibly-incorrect-)labor machine such as an LLM system can indeed save human labor.
AnimalMuppet 2y ago
Because it takes so much work. Good software, even with bugs, released today, can be used today. Perfect software, released two years from now, cannot be used today, or next week, or next year. "Good now" beats "perfect later", at least now, but often it beats it later too. While someone is working on "provably perfect", someone who isn't using that approach has released four versions that were not perfect, but were good enough to be useful. That person took the market, and when the provably perfect version finally comes out, nobody cares, because they're used to how the other one works, and it has more features. And if the "provably perfect" person wants to implement those features, they have to change the program, which means they have to re-do the proof...
- kimixa 2y ago
  Also "perfect software" doesn't actually mean "perfectly robust systems" - at the end of the day it has to interact with the Real World, and the Real World is messy. You still have to cope with failures from cosmic rays, power brownouts, hardware bugs (or at least a difference in specification of the hardware to the model used for this sort of formal verification), failures communicating with other devices etc. So critical software already has to deal with failures and recover, no amount of formal verification will remove that requirement.
  - AnimalMuppet 2y ago
    And unexpected input from other systems. And if it was unexpected in a way that wasn't covered by your proof, then your program is not guaranteed to work correctly on that input. And the real world has a lot of ways for input to do unexpected things...
  - unification_fan 2y ago
    > You still have to cope with failures from cosmic rays Much like you have to cope with hash or GUID collisions... that is, you don't, because it statistically never happens. Unless you're speedrunning super mario or something. Besides if you have a program that's formally verified, you just need to do what NASA did for its Apollo missions and make all the logic redundant and gate it behind a consensus algorithm. You can argue that all 4 computers might get hit by a cosmic ray in just the right place and at just the right time... But it will never ever happen in the history of ever. So my point is that the real world is messy. But the systems we design as engineers are not necessarily as messy. And the interface between the real world and our systems can be managed, and the proof of it is that we wouldn't be chatting across an entire ocean by modulating light itself if that weren't the case.
    - AlotOfReading 2y ago
      I've definitely dealt with hash/GUID collisions in the context of safety critical systems before. It's not a particularly uncommon requirement either. "just" is pulling a lot of weight in your comment. Redundant consensus is difficult and expensive, all to address very particular error models (like the one you're assuming). If we expand our error model from localized error sources like cosmic rays to say, EMI, there are entire categories of fault injection attacks well-known to work against modern redundant systems. That's assuming your specification is comprehensive and correct in the first place of course. My experience is that all specifications have holes related to their assumptions about the real world, and many of them have bugs or unintended behavior as well.
- unification_fan 2y ago
  But you don't have to do the proving. You can let someone who is, like, REALLY good at formal verification do it and then benefit from the libraries they produce Verification is useful when you're dealing with low level or very declarative stuff. You don't really have to "verify" a CRUD repository implementation for a random SPA. But the primitives it relies on, it would be good if those were verified.
  - AnimalMuppet 2y ago
    Same problem. Sure, it would be great if the primitives we use were proven correct. But I've got stuff to write today, and it doesn't look like the proven-correct primitives are going to arrive any time soon. If I wait for them, I'm going to be waiting a long time, with my software not getting written.
    - ted_dunning 2y ago
      The memory safety of the Rust standard library is an example of something where formal methods are bearing fruit already. So you don't necessarily have to wait.
thaumasiotes 2y ago
> What it does is guarantee correctness which is like the holy grail for programmers. Formal verification can never guarantee correctness. For that to happen, you'd need to know that the property you verified is the property you want. If you have the ability to write correct specifications, you also have the ability to write correct programs, and running the verification doesn't add any value.
- rocqua 2y ago
  Correctness is taken to mean "The program matches its specification". Or, more literally, "the program is a correct implementation of it's specification".
  - LegionMammal978 2y ago
    Taking the reductio ad absurdum, the program itself perfectly specifies its own behavior. Yet it's hardly something I'd point to as a holy grail. We want programs that do what we want them to, which is generally a human construct rather than a technical one. (And you'd better hope that two different people don't expect the program to do two different things in the same situation!)
    - schoen 2y ago
      Huh, this is kind of like other trivial objects in mathematics (typically the empty object and the universal object). One trivial property is "this program computes what this program computes" while the other trivial property is probably "this program computes something". Although these are themselves only trivial in a programming language in which every string represents a valid program.
    - not2b 2y ago
      There are other ways to exploit formal verification. For example, you may be able to formally prove that the unoptimized version of your program has the same behavior as the optimized version, subject to specified constraints. This can assure that there aren't any bugs in the optimization that affect program correctness. You're eliminating a class of bugs. Of course, it's possible that the unoptimized version is incorrect, but at least you can assure that your aggressive optimization approach didn't cause breakage. Such approaches are commonly used for hardware verification.

twinkjock 2y ago

This is why connecting formal verification to an infinite (possibly-incorrect-)labor machine such as an LLM system can indeed save human labor.

AnimalMuppet 2y ago

Because it takes so much work. Good software, even with bugs, released today, can be used today. Perfect software, released two years from now, cannot be used today, or next week, or next year. "Good now" beats "perfect later", at least now, but often it beats it later too. While someone is working on "provably perfect", someone who isn't using that approach has released four versions that were not perfect, but were good enough to be useful. That person took the market, and when the provably perfect version finally comes out, nobody cares, because they're used to how the other one works, and it has more features. And if the "provably perfect" person wants to implement those features, they have to change the program, which means they have to re-do the proof...

kimixa 2y ago
Also "perfect software" doesn't actually mean "perfectly robust systems" - at the end of the day it has to interact with the Real World, and the Real World is messy. You still have to cope with failures from cosmic rays, power brownouts, hardware bugs (or at least a difference in specification of the hardware to the model used for this sort of formal verification), failures communicating with other devices etc. So critical software already has to deal with failures and recover, no amount of formal verification will remove that requirement.
- AnimalMuppet 2y ago
  And unexpected input from other systems. And if it was unexpected in a way that wasn't covered by your proof, then your program is not guaranteed to work correctly on that input. And the real world has a lot of ways for input to do unexpected things...
- unification_fan 2y ago
  > You still have to cope with failures from cosmic rays Much like you have to cope with hash or GUID collisions... that is, you don't, because it statistically never happens. Unless you're speedrunning super mario or something. Besides if you have a program that's formally verified, you just need to do what NASA did for its Apollo missions and make all the logic redundant and gate it behind a consensus algorithm. You can argue that all 4 computers might get hit by a cosmic ray in just the right place and at just the right time... But it will never ever happen in the history of ever. So my point is that the real world is messy. But the systems we design as engineers are not necessarily as messy. And the interface between the real world and our systems can be managed, and the proof of it is that we wouldn't be chatting across an entire ocean by modulating light itself if that weren't the case.
  - AlotOfReading 2y ago
    I've definitely dealt with hash/GUID collisions in the context of safety critical systems before. It's not a particularly uncommon requirement either. "just" is pulling a lot of weight in your comment. Redundant consensus is difficult and expensive, all to address very particular error models (like the one you're assuming). If we expand our error model from localized error sources like cosmic rays to say, EMI, there are entire categories of fault injection attacks well-known to work against modern redundant systems. That's assuming your specification is comprehensive and correct in the first place of course. My experience is that all specifications have holes related to their assumptions about the real world, and many of them have bugs or unintended behavior as well.
unification_fan 2y ago
But you don't have to do the proving. You can let someone who is, like, REALLY good at formal verification do it and then benefit from the libraries they produce Verification is useful when you're dealing with low level or very declarative stuff. You don't really have to "verify" a CRUD repository implementation for a random SPA. But the primitives it relies on, it would be good if those were verified.
- AnimalMuppet 2y ago
  Same problem. Sure, it would be great if the primitives we use were proven correct. But I've got stuff to write today, and it doesn't look like the proven-correct primitives are going to arrive any time soon. If I wait for them, I'm going to be waiting a long time, with my software not getting written.
  - ted_dunning 2y ago
    The memory safety of the Rust standard library is an example of something where formal methods are bearing fruit already. So you don't necessarily have to wait.

thaumasiotes 2y ago

> What it does is guarantee correctness which is like the holy grail for programmers. Formal verification can never guarantee correctness. For that to happen, you'd need to know that the property you verified is the property you want. If you have the ability to write correct specifications, you also have the ability to write correct programs, and running the verification doesn't add any value.

rocqua 2y ago
Correctness is taken to mean "The program matches its specification". Or, more literally, "the program is a correct implementation of it's specification".
- LegionMammal978 2y ago
  Taking the reductio ad absurdum, the program itself perfectly specifies its own behavior. Yet it's hardly something I'd point to as a holy grail. We want programs that do what we want them to, which is generally a human construct rather than a technical one. (And you'd better hope that two different people don't expect the program to do two different things in the same situation!)
  - schoen 2y ago
    Huh, this is kind of like other trivial objects in mathematics (typically the empty object and the universal object). One trivial property is "this program computes what this program computes" while the other trivial property is probably "this program computes something". Although these are themselves only trivial in a programming language in which every string represents a valid program.
  - not2b 2y ago
    There are other ways to exploit formal verification. For example, you may be able to formally prove that the unoptimized version of your program has the same behavior as the optimized version, subject to specified constraints. This can assure that there aren't any bugs in the optimization that affect program correctness. You're eliminating a class of bugs. Of course, it's possible that the unoptimized version is incorrect, but at least you can assure that your aggressive optimization approach didn't cause breakage. Such approaches are commonly used for hardware verification.