It can be quite a bit of work but the pay-off can not be over-estimated.
Exactly. Where invariants pay off is maintenance. The original programmer intent has been forgotten and is not visible in the code.
I know a big project which hit this wall. There's delicate C++ code with internal inconsistency bugs, and the company can't fix them.
Testcases can supply this function, as well as counters set up for that purpose (statsd or something to that effect).
Once you have enough of those you can (slowly) start to make changes to observe the effects, and once you understand the codebase add more invariants that you have now determined should exist.
The last project where I took that approach (about 4 years ago now) went from 'intractable' to 'stable' in a relatively short time but it required a lot of thinking and some really hard work to get it there.
Much better if your language/platform supports that sort of thing out of the box, even better if it can be done across subsystems.
I am a big proponent and a fan of gradual refactoring -- even if you simply add a feature that can be forced in (which I never do).
But I am always to open learn some more techniques. And I have to admit with a heavy heart that I never really studied computer science... :(
(Planning to fix that but still have no idea where to even start.)
C/C++ has too much undefined behavior. Ada died off. The scripting languages don't need it as much. Rust had potential for proof work, but went off in a different direction. There are modern proof systems, but they're rarely integrated with the programming language.
On the verification side, it's never had more users that I'm aware of. SPARK and Frama-C are very active compared to almost non-existent use of formal methods in industry decades ago. Rust could similarly have a subset integrated with Why3 platform to make the formal methods easier to use. Further, I've seen extraction done from Coq to C and Rust. There's also one person modeling C in WhyML to write the algorithms in the latter but extract to former. Or something like that. Could be done for Rust, too.
Which direction is that?
For some reason, the moment you bring up mathematical thinking, most programmers shy away and claim that this isn't something they should work with 'everyday'.
I never studied CS and I deeply regret that now. I want to up my game and I don't want to always just patch stuff around to infinity, but I honestly have no idea where to start.
What's so wrong with functional languages? I am sure you have heard this cliche a lot but here it comes once more -- I became a much better programmer once I learned an FP language.
Still, back in my Java days I achieved this with a ton of defensive coding, always doing deep cloning before passing complex data structures to anywhere, and trying to enforce design by contract (interfaces and their implementation classes)... which are practically the patterns that any average FP language uses: pattern-matching, immutability and always copying data and thus never passing stuff by reference (always by value), and behaviours / protocols / macros (of the manipulating the AST kind, not in the way C does it).
So to be fair, you are bound to land at an FP language eventually. Maybe you just don't know it yet. Which is fine, learning is about the journey and not the destination anyway.
http://infohost.nmt.edu/~al/cseet-paper.html
https://pdfs.semanticscholar.org/12d5/23e586ffde5cbe020cb3fa...
(Second link has a table and description showing the results they got. Stavely's book distills it into lightweight, less-processy form.)
Design by Contract itself is like assertions on steroids. If your language lacks support, you can build it into your functions at beginning, middle and end. If OOP language, you might use constructors and destructors. If trying to understand it, I have a link that you can give even to project managers.
https://www.win.tue.nl/~wstomv/edu/2ip30/references/design-b...
One benefit of making it a formal spec is you can generate tests directly from your specs. This is an old, old technique being rediscovered recently. Various names include specification-based, model-based, contract-based, and property-based test generation. The last thing you can do is manually or automatically convert your specs into runtime checks for the above and/or fuzz testing. The failure takes you exactly to the property that failed if it was one of them.
Finally, for just the most critical things, you can try formal proof on them. SPARK Ada is a great example used in industry with the book being pretty easy to follow.
https://www.amazon.com/Building-High-Integrity-Applications-...
The nice thing about that toolset, esp the proprietary version, is that you can use automated provers to avoid having to do mathematical proof by hand. If something doesn't pass, you have several options: do some manual work on hints to the automated provers or actual proofs in a proof assistant; monkey around with the code to see if different structure or algorithm gets it through; put in runtime checks for just the properties you couldn't prove. If you do the last one and keep programming while solvers run, then the productivity is similar to Design-by-Contract with the extra benefit some properties might hold in all cases. You might also get performance boost by reducing unnecessary, safety checks via proofs that were successful.
This stuff is useful is when you have lots of modifiable data structures which need to be consistent. Window managers. Operating systems. Game engines. Database internals. Most of the things you need to prove are trivial. But you need tools to check that invariant A is maintained by code far distant from where invariant A is defined. Maintenance programmers will miss that.
[1] http://www.animats.com/papers/verifier/verifiermanual.pdf