On the Business of Proof - Byron Cook
Workshop on Dependable and Secure Software Systems 2021
With only a few niche exceptions, the software industry has not yet figured out how to make deep use of formal mechanical reasoning based on mathematical logic. At Amazon we’ve recently seen tremendous adoption of the approach by product groups, with a variety of customer-facing launches that use automated reasoning, and numerous internal proof projects. This talk attempts to capture aspects of why Amazon has been successful where others have been less so, with the hope of finding working models that can be applied in organizations outside of Amazon.