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