Formal methods are useful for providing irrefutable and credible evidence in the design and implementation of web service features. The use of formal specification and verification models in the design of adaptable complex systems for the rapidly changing conduct and growth of businesses is not straightforward. Beyond the standard techniques that industries use to verify the trustworthiness and security of systems, what are the practical and formal approaches to the design of reliable, complex real-world software such as public cloud services? Newcombe et al. address this nontrivial question by presenting the formal methods that design engineers at Amazon have used over the years to provide security and reliability in complex software systems.

The authors emphasize: (1) the consistent use of design and code reviews by systems engineers to provide robust security and fault-tolerance in complex systems; (2) the importance of selecting a relevant language for the formal design specification and verification of any complex system; (3) the use of an appropriate formal language for identifying elusive software defects, to help increase software performance without jeopardizing accuracy; (4) the benefits of using formal languages to provide safe and accurate responses in complex software; and (5) the ability to recognize the limitations of current formal models in predicting future behaviors in evolving software systems.

Clearly, the authors outline new challenges for the educators of future robust software system designers. Certainly, educators of future software engineers ought to be exposing students to the discrete mathematics and elements of set theory that are required for understanding formal design and specification languages. Future software engineers ought to understand the use of formal methods in the correct design and better implementation of complex systems. I encourage all complex software designers and educators to read and take advantage of the practical ideas in this article.