Making Software 'Correct by Construction' - Professor Martyn Thomas CBE

TL;DR

By using correct by construction methods, software developers can create virtually bug-free software, as demonstrated by companies that routinely produce such software and offer guarantees.

Transcript

this this was said by edar dyra uh 45 years ago and what I hope to do in this lecture is to show that he was right uh and that although he thought that by the end of the 1970s so just 8 years away from when he was was writing and speaking um people would be able to develop software that was virtually bug free by using the kind of methods that he wa... Read More

Key Insights

• 🥶 Correct by construction methods can lead to the production of virtually bug-free software, as demonstrated by companies that routinely produce such software and offer guarantees for its performance.
• 👻 Formal statements and mathematics are used to specify system requirements and allow for analysis and proof of software behavior, providing verifiable evidence of correctness.
• 👨‍💻 Companies that employ correct by construction methods can significantly reduce testing costs, improve code quality, and increase productivity.
• 👱 Correct by construction methods have been successfully applied in various industries, including aerospace, military, and air traffic control.
• 🖤 The resistance to using correct by construction methods is due to various factors, including a lack of belief in its value and a lack of commercial pressure to improve software quality.

Questions & Answers

Q: What is correct by construction?

Correct by construction is an approach to software development that focuses on building software that does exactly what it's required to do, with verifiable evidence of its correctness.

Q: How can companies offer guarantees for virtually bug-free software?

Companies that employ correct by construction methods are able to produce software with extremely low defect rates, allowing them to offer guarantees for its performance and reliability.

Q: What is the role of formal statements and mathematics in correct by construction methods?

Formal statements, using relatively basic mathematics, are used to precisely define the system's requirements and operations, allowing for analysis and proof of software behavior and providing verifiable evidence of correctness.

Q: Why do some companies resist using correct by construction methods?

Companies may resist using correct by construction methods due to a lack of belief in its value, a lack of commercial pressure to improve software quality, or fears that training programmers in these methods will lead to higher turnover.

Summary & Key Takeaways

• Correct by construction methods advocate for software that does exactly what it's required to do and provides verifiable evidence of its correctness.

• Companies that employ correct by construction methods are able to produce virtually bug-free software and offer guarantees as part of their normal business activities.

• The use of formal statements and mathematics in the development process allows for analysis and proof of software behavior, providing verifiable evidence of correctness.