Software doesn't have to be safety critical in order to do harm. Security vulnerabilities, data loss... these all cause harm to the public interest. Whether by

Software doesn't have to be safety critical in order to do harm. Security vulnerabilities, data loss... these all cause harm to the public interest. Whether by snooping, lost profits, online harassment -- these are problems we would be seeing less of if software developers took the view to construct software with fewer errors in the design stage. We simply do not because the practice of writing high-level specifications in the form of mathematical models or proofs is not common. I think the tools have become sophisticated enough and the maths approachable enough that it should be and can be used in the construction of non-safety-critical systems.