Theorem Provers: One Size Fits All?
Logic in Computer Science
2025-09-19 v1 Programming Languages
Abstract
Theorem provers are important tools for people working in formal verification. There are a myriad of interactive systems available today, with varying features and approaches motivating their development. These design choices impact their usability, alongside the problem domain in which they are employed. We test-drive two such provers, Coq and Idris2, by proving the correctness of insertion sort, before providing a qualitative evaluation of their performance. We then compare their community and library support. This work helps users to make an informed choice of system, and highlight approaches in other systems that developers might find useful.
Keywords
Cite
@article{arxiv.2509.15015,
title = {Theorem Provers: One Size Fits All?},
author = {Harrison Oates and Hyeonggeun Yun and Nikhila Gurusinghe},
journal= {arXiv preprint arXiv:2509.15015},
year = {2025}
}