Almost every point here reads the exact same if you replace “formal methods” with “tests” or “static types”. I’d want to see a discussion of the unique limitations and powers of FM.
((Also, which FM is he talking about? Code verification? Design verification? Correct-by-Construction?))
Static types are clearly a special case of formal methods.
Tests could be construed as such, too—weaker on the quantification, but stronger on the computation.
If these are the only ones you’re using, you’re missing out. Big time. Especially if you’re programming in a high-stake, irreversible environment where your bug budget is zero.
(Disclaimer: I’m the author of the original article linked.)
Tests could be construed as such, too—weaker on the quantification, but stronger on the computation.
That’s going too far. They should be kept separate in most discussions if manual since they’re almost always exploring a tiny fraction of the state space formal verification would. Spec/model/property-based testing is a hybrid where they start with a formal property but test some percentage of inputs for it. I call that lightweight, formal method with extra emphasis that it can miss stuff,
“Formal methods help you make explicit what your assumptions and your guarantees are and ruthlessly eliminate any flaw between the assumptions and guarantees.”
Well put! I might quote them on that in future.
EDIT this one, too:
“Formal methods will prevent the multiplication of implicit assumptions you don’t know about, don’t track, and don’t check as your system evolves, that may once have been true yet will cause catastrophic errors when they stop being valid (see Ariane V).”
Almost every point here reads the exact same if you replace “formal methods” with “tests” or “static types”. I’d want to see a discussion of the unique limitations and powers of FM.
((Also, which FM is he talking about? Code verification? Design verification? Correct-by-Construction?))
Static types are clearly a special case of formal methods. Tests could be construed as such, too—weaker on the quantification, but stronger on the computation. If these are the only ones you’re using, you’re missing out. Big time. Especially if you’re programming in a high-stake, irreversible environment where your bug budget is zero.
(Disclaimer: I’m the author of the original article linked.)
That’s going too far. They should be kept separate in most discussions if manual since they’re almost always exploring a tiny fraction of the state space formal verification would. Spec/model/property-based testing is a hybrid where they start with a formal property but test some percentage of inputs for it. I call that lightweight, formal method with extra emphasis that it can miss stuff,
[Comment removed by author]
“Formal methods help you make explicit what your assumptions and your guarantees are and ruthlessly eliminate any flaw between the assumptions and guarantees.”
Well put! I might quote them on that in future.
EDIT this one, too:
“Formal methods will prevent the multiplication of implicit assumptions you don’t know about, don’t track, and don’t check as your system evolves, that may once have been true yet will cause catastrophic errors when they stop being valid (see Ariane V).”