I’m not super experienced with formal verification, but I did dip my toes in it a few times.
My impression is that it’s far from a magic bullet. Writing formal specs is basically like writing the code/tests just differently. And the more it covers the more it becomes the same thing. And it suffers from the same problems.
My conclusion every time was that the code itself is the formal spec and the formal spec is the code.
By analogy with construction, the code is both the building and the blueprint.
> My conclusion every time was that the code itself is the formal spec and the formal spec is the code.
Yes you can end up with tautological specs, where it's more or less a copy of the code. E.g. you aren't going to benefit much from formally verifying `max()`.
But there are many many cases where the formal specification is much much simpler and more obviously correct than the actual code. The classic examples are:
* Any kind of encoding / decoding transformation has the property `decode(encode(x)) == x`.
* Sorting: any sorting algorithm should result in a sorted array (forall i, j: i < j --> array[i] <= array[j])
I also think universal quantifiers ("for all ...") are a key distinguishing feature of specs. For example, a spec for a shortest path algorithm can be much simpler than any actual algorithm, largely because we can quantify over all (potentially infinitely many) paths:
This. In my very limited experience (i didn't write the code or specs), I've seen the runtime code find more bugs in the formal specs than the formal specs finding bugs in the runtime code.
My impression is that it’s far from a magic bullet. Writing formal specs is basically like writing the code/tests just differently. And the more it covers the more it becomes the same thing. And it suffers from the same problems.
My conclusion every time was that the code itself is the formal spec and the formal spec is the code.
By analogy with construction, the code is both the building and the blueprint.