Coqatoo: Generating Natural Language Versions of Coq Proofs

TL;DR

Coqatoo is a tool designed to convert formal Coq proofs into natural language, making them more accessible and understandable, especially for users less familiar with formal proof syntax.

Contribution

This paper introduces Coqatoo, a novel tool that automatically translates Coq proofs into natural language, enhancing readability and accessibility of formal proofs.

Findings

Coqatoo successfully generates natural language descriptions of Coq proofs.

The tool improves understanding for less-experienced users.

It demonstrates potential for broader adoption of formal proofs.

Abstract

Due to their numerous advantages, formal proofs and proof assistants, such as Coq, are becoming increasingly popular. However, one disadvantage of using proof assistants is that the resulting proofs can sometimes be hard to read and understand, particularly for less-experienced users. To address this issue, we have implemented a tool capable of generating natural language versions of Coq proofs called Coqatoo, which we present in this paper.