For many decades, formal methods are considered to be the way forward to help the software industry to make more reliable and trustworthy software. However, despite this strong belief and many individual success stories, no real change in industrial software development seems to be occurring. In fact, the software industry itself is moving forward rapidly, and the gap between what formal methods can achieve and the daily software-development practice does not appear to be getting smaller (and might even be growing). In the past, many recommendations have already been made on how to develop formal-methods research in order to close this gap. This paper investigates why the gap nevertheless still exists and provides its own recommendations on what can be done by the formal-methods-research community to bridge it. Our recommendations do not focus on open research questions. In fact, formal-methods tools and techniques are already of high quality and can address many non-trivial problems; we do give some technical recommendations on how tools and techniques can be made more accessible. To a greater extent, we focus on the human aspect: how to achieve impact, how to change the way of thinking of the various stakeholders about this issue, and in particular, as a research community, how to alter our behaviour, and instead of competing, collaborate to address this issue.

翻译：数十年来，形式化方法始终被认为是帮助软件行业构建更可靠可信软件的有效途径。尽管这种信念根深蒂固且涌现出诸多成功案例，工业界的软件开发实践却并未出现实质性变革。事实上，软件行业自身正在快速发展，形式化方法所能达到的目标与日常软件开发实践之间的差距非但没有缩小，反而可能正在扩大。过去已有很多关于如何开展形式化方法研究以弥合这一差距的建议。本文探究该差距持续存在的根本原因，并就形式化方法研究群体如何搭建沟通桥梁提出建议。我们的建议并非聚焦于开放研究问题——事实上，当前形式化方法的工具与技术已具备相当水准，能够解决众多非平凡问题；我们确实提出了若干提升工具与技术易用性的技术性建议。但更重要的是，我们着重关注人文层面：如何实现影响力，如何转变各利益相关方对此问题的思维方式，特别是研究群体如何改变自身行为——从相互竞争转向协作，共同应对这一挑战。