Bringing Formal Verification into Widespread Programming Language Ecosystems
S. Juhošová (TU Delft - Electrical Engineering, Mathematics and Computer Science)
J.G.H. Cockx – Mentor (TU Delft - Programming Languages)
C. Lofi – Graduation committee member (TU Delft - Web Information Systems)
L.F.B. Escot – Coach (TU Delft - Programming Languages)
More Info
expand_more
Dataset containing the raw answers to the user study questionnaire.
https://doi.org/10.4121/611fd9e6-a7bb-47d7-9afe-34efe890ddd7The GitHub repository containing the programming assignments used during the user study.
https://github.com/sarajuhosova/agda2hs-user-study/The GitHub repository containing source code for Agda2HS - a tool that was investigated and improved as part of this thesis.
https://github.com/agda/agda2hsOther than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.
Abstract
Formal verification is a powerful tool for ensuring program correctness but is often hard to learn to use and has not yet spread into the commercial world. This thesis focuses on finding an easy-to-use solution to make formal verification available in popular programming language ecosystems. We propose a solution where users can write code in an interactive theorem prover and then transpile it into a more popular programming language. We use Agda2HS as a case study to determine what challenges users find in using such a tool, improve selected features, and then conduct a user study to evaluate the usability. We find that detailed documentation, support for commonly-used features in the target programming language, features that facilitate verification, integration of the tool into the target ecosystem, and user studies are necessary for the accessibility of such a tool.