[unification_fan]

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.

[thaumasiotes]

> 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.

[tristramb]

It guarantees correctness relative to a given requirement.

The real value of formal proofs lies in forcing you to think deeply about the requirement and your implementation of it and to make your assumptions about it explicit.

I have only ever used proof once in my career. We had a problem with an aircraft main computer that it was occasionally failing during start up and then refusing start again on all subsequent restarts. It was a multiprocessor computer and each processor was running start up tests some of which would interfere if run at the same time. I was worried that if the start-up was stopped at an arbitrary time it might leave the control variables in a state that would prevent further start-ups. I used Leslie Lamport's first technique (https://lamport.azurewebsites.net/pubs/pubs.html#proving) in an attempt to prove that it would always start up no matter at what point it was stopped the previous run. But I was unable to complete the proof in one situation. So I added a time delay to the start-up of some of the processors to ensure that this situation never occured. But that didn't fix the original problem. That turned out to be a hardware register being read before it had settled down. I fixed that later.

[thaumasiotes]

> It guarantees correctness relative to a given requirement.

OK, but given that you don't know what that requirement is, how does that help you?

[ted_dunning]

But you do know the specification, or at least parts of it in many cases.

In the upstream example, one specification is that some reasonable time after you turn on the airplane, the flight controller is ready to fly. That's a very reasonable spec and important to verify in the given story. It is a thin end of the wedge for a lot of real-time guarantees that you might like to make.

As another instance where the specification is known, what is the specification of compiled object code? The specification of compiled code is the source code and proving that the object code matches the source code is a way to protect against adversarial tool chains. Check out seL4 for an example of this kind of formal verification.

Memory safety is another property susceptible to formal verification. The Rust community is making use of this very nicely.

The net lesson is that even if it is impossible to get formal specifications for lots of things, there are lots of other things where you can define good specifications (and you might be able to prove you meet them, too!).

[rocqua]

Correctness is taken to mean "The program matches its specification". Or, more literally, "the program is a correct implementation of it's specification".

[LegionMammal978]

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!)

[not2b]

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.

[schoen]

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.

[pegasus]

The program includes a lot of incidental complexity which would not be part of the spec. For example, for a sort function, the spec would be the "array sorted" postcondition. The code OTOH could be arbitrarely complex.

[zozbot234]

To be clear, the proper postcondition for a sort function is "the output array is a permutation of the input array and it is sorted".

[e2021]

how do you know the specification is correct? Its turtles all the way down here

[AnimalMuppet]

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]

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.

[unification_fan]

> 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]

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.

[AnimalMuppet]

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]

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]

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]

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.

[twinkjock]

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