The point would be to prove that your database stays consistent, a DB upgrade wouldn't break, or that you could achieve 100% up time given certain assumptions. An automated solver/prover might even be able to tell you where in your program breaks this. Without a technology like this, you have to carefully read your program, but this is the methodology to make the computer deal with that. Unfortunately formal verification is mostly used for research, F* is framing itself as taking a step to bring that to production codebases. Unfortunately I don't know good resources, but as researchers adapt this technology, and as we automate a lot of the heavy mathematics, you'd never want a programming language without this option.