Theorem Provers: One Size Fits All?
This paper compares the Coq and Idris2 interactive theorem provers to provide a qualitative evaluation of their performance via a proof of the correctness of insertion sort. The paper’s key contribution is comparing these systems through a user experience lens, rather than purely the underlying logic upon which the system relies.