2 ms·

I think my main point is that writing the specification is difficult enough with a non-trivial program with property tests, with many places tending to even avo

I think my main point is that writing the specification is difficult enough with a non-trivial program with property tests, with many places tending to even avoid it if they can. If formal verification is even more difficult, it doesn't matter that it has more power and can make the code even more correct - the cost is a huge blocker.

Jtsummers 2y ago
It depends on how you do the formal verification. There are systems like SPARK/Ada which brings the specification into the language you're developing in (supports only a subset of Ada, but every year they're expanding what it covers), JML which does something similar for Java but the specification language is expressed in its own notation in Java comments, and others. If you use these kinds of systems you can be more judicious in what you try to prove. Whole program proofs are infeasible (or at least impractical) generally, but you pick the subsets you care about most and you can add annotations and prove them (automatically ideally, but you can bring in an external proof assistant as well). You leave the rest of the system to testing which has proven remarkably effective over the decades (when taken seriously, at least). This isn't an all-or-nothing proposition, you choose how to spend your time and effort with formal verification just like you do with testing or other work.
clarus 2y ago
There are some specifications that are always there, like the absence of reachable panics or the backward compatibility between releases on stable entry points. Otherwise you can outsource this work to specialized companies such as Formal Land or others!
muldvarp 2y ago
> the cost is a huge blocker. It is. Formal verification is and will be (for a very long time) a thing you only do for airplanes and nuclear reactors.

2 ms·

I think my main point is that writing the specification is difficult enough with a non-trivial program with property tests, with many places tending to even avo

by vlovich123 2y ago

Jtsummers 2y ago
It depends on how you do the formal verification. There are systems like SPARK/Ada which brings the specification into the language you're developing in (supports only a subset of Ada, but every year they're expanding what it covers), JML which does something similar for Java but the specification language is expressed in its own notation in Java comments, and others. If you use these kinds of systems you can be more judicious in what you try to prove. Whole program proofs are infeasible (or at least impractical) generally, but you pick the subsets you care about most and you can add annotations and prove them (automatically ideally, but you can bring in an external proof assistant as well). You leave the rest of the system to testing which has proven remarkably effective over the decades (when taken seriously, at least). This isn't an all-or-nothing proposition, you choose how to spend your time and effort with formal verification just like you do with testing or other work.
clarus 2y ago
There are some specifications that are always there, like the absence of reachable panics or the backward compatibility between releases on stable entry points. Otherwise you can outsource this work to specialized companies such as Formal Land or others!
muldvarp 2y ago
> the cost is a huge blocker. It is. Formal verification is and will be (for a very long time) a thing you only do for airplanes and nuclear reactors.