alt Hacker NewsMy 2c I don't understand any of the material I've read describing them. What I do understand makes them sound like it will be a load of work for questionable benefits. If I end up writing safety-critical code. (Aerospace firmware, big robots etc), I will get over this hump and learn them. If not, I am not yet compelled; rather intimidated.
Maybe this is like Quaternions, that are actually very easy and useful, but suffer from confusing descriptions. Or maybe more like Monads, which are actually very abstract, and may not be suitable unless your the sort who understands Mathematician style mathematics.
More to the point: I'm not even sure how I would get started and evaluate them tacitly.
Of particular confusion: Does formal verification lead to a strange-loop style or "It's verification all the way down" scenario, where you are shifting the correctness from the original code to the verification? Then must verify the verification ad-infinitum? (This is almost certainly wrong, but I don't grasp why)
The big question I ask: "Would I rather have a code base with formal verification, or one in which all the time and effort used by add that were spent using and testing the software in a practical way; or code reviewing it"
> Does formal verification lead to a strange-loop style or "It's verification all the way down" scenario, where you are shifting the correctness from the original code to the verification? Then must verify the verification ad-infinitum?
IANA formal methods guy, but my understanding is: yes, you're shifting the correctness burden from the code to the spec.
So why is that better? Because the spec is much shorter and more focused -- it strips out all of the implementation details.
It's bad to say "you have to trust this 100,000 line program." It's much better to say "you have to trust this 100 line spec, and the code that verifies it."