[agentultra]

Something I've become passionate about in the last couple of years is reliability in software and professionalism in software development.

I feel like we're at an inflection point where the cost of developing formal specifications is coming down enough for more teams to be using them in their practice. I'd like to continue that trend to allow more developers to use pure maths to solve their problems and use computers to verify (and maybe synthesize) their work.

I don't know what five years from now will look like but I'd like to either be working on or finishing a maths degree or starting a company to work on developing tools to work with formal specifications and proof automation and consulting with teams to help them write specifications for their critical components.

> How do you work towards achieving it?

I spend my free time working on problems in predicate calculus and writing specifications in TLA+ or Lean. I look for opportunities in my day-to-day work that would benefit from those skills. When it is time to think about my next position I will look for jobs that will help me get to that next level. Right now that means looking for opportunities to work on projects where reliability is highly desired and complexity is also quite high.

When I conduct 1-on-1's with my team I try to get people to think about their career. I like to encourage people to think strategically about their future. What do you want to be doing, in an ideal world, 2-3 years from now? What can we do now to set you up to be ready for that opportunity when it comes up?

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