And that's why we need good tools for reasoning about and specifying systems. Amazon and Microsoft seem to trust TLA+ for designing some of the most complex sy

And that's why we need good tools for reasoning about and specifying systems. Amazon and Microsoft seem to trust TLA+ for designing some of the most complex systems in production today. I'm pretty sure they wouldn't have pulled it off without formal methods (Amazon released a paper about their use of TLA+ and MS has mentioned it's role in the development of Cosmos). Software systems can be specified using precise, robust blueprints. Those blueprints are expressed in math and I believe from my own experience that they are immensely useful.