[hasana]

This is something I think about from time to time as well, I haven't been able to see how to actually implement this in a real project. When I studied Computer Science, I had a particular interest in formal design, (studied Eiffel breifly) but haven't seen that aspect of it translate into my work. I work in enterprise web application development, and the way projects are estimated, resourced and budgeted (in my experience) doesn't seem to offer any opportunities to try this. (Or I just haven't been smart enough to make a plan). How would you go about creating a formal specification, to build something like a Facebook Messenger bot for an e-commerce store? Or something simpler like a Angular driven warehouse catalog application?

[Jtsummers]

If you're new to it, focus on formally specifying parts and not the whole system. These sorts of specifications can become very complex very quickly. And if you're modeling them, the time to execute a model could take an inordinate amount of time.

For your two examples, rather than modeling how you communicate with Facebook for the bot, focus on how the bot gets data to and from your e-commerce store and how they stay synchronized or consistent. Your communication with Facebook's services may not even make it into your model. For the angular driven warehouse catalog application, same thing. You don't need to model angular and the UI. You need to model how the data gets to and from the UI and stays consistent with the warehouse catalog.

[agentultra]

> 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.