Comment by mjorgers
11 hours ago
It might be that I’m unfamiliar with the matter, but as I understand it, in order to prove a statement, the statement must correctly model the reality of the code. In that case, how can you be truly sure that, when formally verifying a program, you have correctly modelled the software you’re trying to verify?
Couldn’t it very well be that you proved something that wasn't actually your program?
If you have a model of the programming language, then you can make proofs about the source code itself. At this point, your assumption is that you are accuratly modelling the compiler.
You can go a step farther and model the instruction set and architecture, and which point you can make proofs about the final binary directly (thereby sidestepping the problem of compiler bugs). At this point, your assumption is just that your physical hardware actually matches your model.
> Couldn’t it very well be that you proved something that wasn't actually your program?
Correct. It can happen, where the actual code, could diverge from a lean representation of it, in a glaring or subtle way.
> how can you be truly sure that, when formally verifying a program, you have correctly modelled the software you’re trying to verify?
You can do it backwards. You declare the properties you want the resulting program/function to have, using a proof assistant like Lean, then prove that a program exists that meets those requirements, and the proof assistant spits two things: a confirmation that the proof is valid, and a piece of code that implements the proof, in the form of computer code.
At least that's how the proof assistant Coq would often be used. You still have the challenge of ensuring that you have defined the properties you really want in the first place, but at least it solves the part where you want the code to meet the specification.
I mean ... The thing about formal verification is that you can write the extremely slow but correct version of your code and then have an optimizer write a much more efficient version with a proof of correctness.
For things like programming languages we often have tedious, but slow, semantics that can be directly implemented in a suitable language. Then really all that a compiler or interpreter is is a faster version of those semantics.
If you are able to show correspondence between the fast and the the correct version, then you can toss the correct and slow version without even ever running it and just defer to the provably correct fast version.
Most software is ultimately like this