标题： 使用验证感知编程语言时，开发人员面临哪些挑战？ 显示英文标题

标题： What Challenges Do Developers Face When Using Verification-Aware Programming Languages?

摘要： 软件可靠性在确保我们依赖的数字系统正确运行方面至关重要。 在软件开发中，提高软件可靠性通常涉及测试。 然而，对于复杂且关键的系统，开发人员可以使用契约式设计（DbC）方法来定义软件组件必须满足的精确规范。 验证感知（VA）编程语言在编译时或运行时支持DbC和形式化验证，其正确性保证比传统测试更强。 然而，尽管VA语言提供了强大的保证，它们的采用仍然有限。 在本研究中，我们通过使用主题建模技术分析开发者在公共论坛上的讨论，来研究采用VA语言的障碍。 我们还通过开发者调查来补充这一分析，以更好地了解与VA语言相关的实际挑战。 我们的研究结果揭示了采用VA语言的主要障碍，包括陡峭的学习曲线和可用性问题。 基于这些见解，我们提出了可操作的建议，以提高VA语言的可用性和可访问性。 我们的研究结果表明，简化工具界面、提供更好的教育材料以及改善与日常开发环境的集成，可能会提高这些语言的可用性和采用率。 我们的工作为提高VA语言的可用性并使验证工具更易访问提供了可行的见解。 显示英文摘要

摘要： Software reliability is critical in ensuring that the digital systems we depend on function correctly. In software development, increasing software reliability often involves testing. However, for complex and critical systems, developers can use Design by Contract (DbC) methods to define precise specifications that software components must satisfy. Verification-Aware (VA) programming languages support DbC and formal verification at compile-time or run-time, offering stronger correctness guarantees than traditional testing. However, despite the strong guarantees provided by VA languages, their adoption remains limited. In this study, we investigate the barriers to adopting VA languages by analyzing developer discussions on public forums using topic modeling techniques. We complement this analysis with a developer survey to better understand the practical challenges associated with VA languages. Our findings reveal key obstacles to adoption, including steep learning curves and usability issues. Based on these insights, we identify actionable recommendations to improve the usability and accessibility of VA languages. Our findings suggest that simplifying tool interfaces, providing better educational materials, and improving integration with everyday development environments could improve the usability and adoption of these languages. Our work provides actionable insights for improving the usability of VA languages and making verification tools more accessible.