> Automated theorem proving is the only way to build better machines. That is only true for a very narrow notion of "better machines". Automated theorem provin

> Automated theorem proving is the only way to build better machines. That is only true for a very narrow notion of "better machines". Automated theorem proving is still light years away from being applicable in the majority of software projects. Don't get me wrong I am aware of the progress made in the last decades. Yet, it will be some time until someone writing the next iOS app will reach routinely for an automated theorem prover to lower the defect rate. And even then, the questions remains whether fulfilling a formal specification is at all correlated with "better machines" or "better software". There are domains where this is conceivable: os kernels (L4), certifying compilers (CompCert), and others. But how does a theorem prover, automated or not, help with improving the next generations of video codecs? That is an intrinsically subjective problem -- the quality axis, less so the performance axis. How does theorem proving help with neuronal networks? How does it help with capturing the right business process to actually improve business outcomes and not just introducing new bureaucracy?