| > If you're new to it, focus on formally specifying parts and not the whole system. This. Many detractors of formal methods will claim that software to too complex to specify formally and so it's no use. I believe they are right. Software is quite complex. And that's why you should use tools to help you manage it. When you start building an event-sourced system architecture for your e-commerce system that scales up automatically and never goes offline during a deploy or single component failure... how will you know your design is correct? How will you measure your success? (Yes, TDD encourages a sort-of informal "specification by example" and integration tests catch a lot of errors... but the kinds of things formal specifications have been proven to catch cannot be imagined by a mere mortal... despite the illusions of power programming has given us it is helpful to remember that illusions have no real power. You can write a specification to verify your design is free from race conditions given some context but you cannot anticipate all of the state-transitions that can lead to a race condition if all you're thinking about is the code) This is why I think formal methods are useful and why you don't need to specify the whole system. Nobody is going to care if you have a formal proof that you can copy a file. What is going to be interesting is if you have a high-assurance specification that you can check which demonstrates that given any number of clients and command-dispatching processes eventually an order will be completed and no event will be recorded twice, out of order, or dropped (given that there are at least N dispatcher processes running and what-have-you). It is quite impressive if you can write a proof that if you write your program to maintain certain invariant properties then you do not need to have a lock in your program. You can't prove those things with a bunch of boxes and lines. My advice is to start small and try to work on a specification of a particular component or protocol that matters the most. I like to think about it in terms of risk. I'll ask myself questions like: what is the worst thing that could happen if we get this part wrong? or what part of this system do we have to absolutely ensure is right for the project to succeed? If the answer the first question is not, "maybe someone will be annoyed or the business will find it annoying" then I increment the risk counter in the back of my mind. If the imaginary actuary assessing my project says that the cost of insuring the project against its risk is out-pacing what I can make from completing the project or potentially bringing harm to the business (or people) then I'll take a step back and consider ways to de-risk the project. There are many levers I can pull and I'm glad I have formal methods as I think that the cost of doing that work pays off in spades. Combined with other techniques and tools at our disposal it is much cheaper today to write highly reliable software than it has ever been. |