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

TL;DR

This paper investigates the barriers to adopting Verification-Aware programming languages, revealing challenges like steep learning curves and usability issues, and offers recommendations to enhance their accessibility and adoption.

Contribution

It combines topic modeling of developer discussions with a survey to identify practical challenges and proposes actionable improvements for Verification-Aware languages.

Findings

Steep learning curves hinder adoption.

Usability issues limit practical use.

Improved tools and education can enhance adoption.

Abstract

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.