Here [0] is a concrete example of using a formal verification system ontop of C (and the blog contains many other examples) along with an excellent dialog aroun

Here [0] is a concrete example of using a formal verification system ontop of C (and the blog contains many other examples) along with an excellent dialog around the example. First a caveat, this formal verification system is rather simple, and only proves code within the domain of the C standard. Using such a system with a buggy C compiler (pretty much all of them) or the result on subtly incorrect hardware (like most modern hardware) will still allow for the formal verification to be wrong. But it is an order of magnitude better than writing out pre-post conditions in comments, fuzzing, or automated tests. And slightly better than pure functions: * Pre-post conditions are code and actually enforced at compile time. * All possible cases are tested for correct behavior, no need to stochastically test ranges (fuzzing) when the entire range is proven or specific test cases (unit tests) when every corner case has been proven. * Pure functions can't deal with state. Even monads still require a trap door, this system can still prove through those trap doors rather effectively. Now for the example in question: Note how the formal verification system points out a problem when the pointers match, could a linter notice that? Maybe, but probably not, at best it would be a "potential problem with equal pointers", it would have to actually understand the source code, and the intent of the programmer, like a formal verification system does, to know whether it's an actual problem. The formal verification system knows it's a problem because it deduced it from the rules of the C standard and the code. So coding standards ("Always check for equal pointers when expecting different ones." or "Never call this function with equal pointers.") are a decent workaround. But an order of magnitude better is: "We've proven the code never violates our expectations." Accidentally violating those expectations is the purpose of the coding standards in the first place; we've fixed the root problem so the decent workaround is no longer required. [0] https://critical.eschertech.com/2010/06/22/aliasing-and-how-to-control-it/ https://critical.eschertech.com/2010/06/22/aliasing-and-how-...