Files and links (1)
Preprint (Author's original)arXiv.org - Non-exclusive license to distribute, Open
Preprint
Natural Language Specifications in Proof Assistants
arXiv (Cornell University)
16 May 2022
Abstract
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.
Metrics
8 Record Views
Details
- Title
- Natural Language Specifications in Proof Assistants
- Creators
- Colin S GordonSergey Matskevich
- Publication Details
- arXiv (Cornell University)
- Resource Type
- Preprint
- Language
- English
- Academic Unit
- Computer Science (Computing)
- Other Identifier
- 991021868729704721