3 ms·
I am strongly inclined toward verifying my software to the extent possible but there are many practical challenges. I think academic formal verification methods
by jandrewrogers 4y ago
I am strongly inclined toward verifying my software to the extent possible but there are many practical challenges. I think academic formal verification methods look elegant, which appeals to me, but are extremely human intensive when what I really want to do is throw machines at the problem to the extent possible. There are also some important types of software correctness that are still difficult to capture with these methods, though the state-of-the-art has improved with time.
I've toyed with many methods, tools, techniques, and approaches to get a sense of where the ROI maxima is for my own purposes. In practice, I've found that sophisticated and comprehensive application of less elegant methods amenable to throwing hardware at them, like exhaustive functional testing, thorough fuzzing infrastructure, systematic fault injection coverage, various types of longevity testing, etc when done well often found all the same design flaws as a tractable level of more academic formal verification. Also easier to maintain as code evolves. Furthermore, these less elegant approaches also found the occasional compiler and hardware bug that more elegant formal verification methods typically do not.
I have wondered if developing and standardizing this less elegant tooling to a high level, so that it is easier to be lazy and throw hardware at the problem, would have at least as much impact on software quality as trying to get everyone to apply very academic formal verification methods, with their current limitations and theoretical constraints. As much as I like the concept of very pure formal verification, I lean toward whatever makes maximizing software quality practical and economic.