Natural Language Specifications in Proof Assistants
This addresses the challenge of ensuring accurate formal verification for software developers and mathematicians, though it appears incremental as it builds on existing proof assistant principles.
The paper tackles the problem of verifying software correctness against natural language specifications in proof assistants, where the translation from informal to formal claims is error-prone and difficult to audit, and proposes building support for natural language specifications within existing proof assistants to enhance trust and auditability.
Interactive proof assistants are computer programs carefully constructed to check a human-designed proof of a mathematical claim with high confidence in the implementation. However, this only validates truth of a formal claim, which may have been mistranslated from a claim made in natural language. This is especially problematic when using proof assistants to formally verify the correctness of software with respect to a natural language specification. The translation from informal to formal remains a challenging, time-consuming process that is difficult to audit for correctness. This paper argues that it is possible to build support for natural language specifications within existing proof assistants, in a way that complements the principles used to establish trust and auditability in proof assistants themselves.