Re: Same old
"It (formally verified code) is very hard to do."
It is indeed VERY hard to do. On the positive side, even a failed attempt is likely to be a lot higher quality than typical code. The downsides: It's expensive and quite possibly impractical to do except perhaps for some mission critical components. And it likely won't get you to market very quickly. The management isn't going to like that.
Then there's the issue of how you know the "rigorous" specification is bug free. If it is, why not write a compiler and compile the specification?
Nonetheless, it's possibly the best idea currently available for potentially producing "error-free" code. So long as we all understand the "error-free" doesn't always and inevitably mean that it will do what you need it to do.
BTW Formal Specification was what Edsger Dijkstra was working on when he wrote his "GOTO considered harmful" letter. I think his point -- which I think hardly anyone really understood at the time -- was that practices like jumping in and out of code sequences based on flags was not only likely to add bugs, but was going to make an already extremely difficult verification process much harder.