形式化方法：优秀的工程实践？

亚马逊AWS工程师Marc Brooker在TLA+大会上的主题演讲中力挺形式化方法。他认为，对于大型分布式系统或关键低级系统，形式化方法并非成本高昂的累赘，而是节省时间和金钱的利器。通过减少返工和降低变更成本，形式化设计能显著提高软件开发效率。并非所有软件都适用，例如UI或价格逻辑等对用户需求变化敏感的领域，敏捷开发更合适。但对于需求明确的大型系统，形式化方法能有效降低bug率，提升性能。Brooker推荐了多种工具，包括TLA+、P、Alloy等规范语言，以及模型检测器、验证型编程语言等，并强调形式化方法不仅能保证正确性，还能帮助探索优化方案，避免在正确性和性能之间艰难权衡。