Abstract
Interactive proof assistants are computer programs carefully constructed tocheck a human-designed proof of a mathematical claim with high confidence inthe implementation. However, this only validates truth of a formal claim, whichmay have been mistranslated from a claim made in natural language. This isespecially problematic when using proof assistants to formally verify thecorrectness of software with respect to a natural language specification. Thetranslation from informal to formal remains a challenging, time-consumingprocess that is difficult to audit for correctness. This paper argues that itis possible to build support for natural language specifications withinexisting proof assistants, in a way that complements the principles used toestablish trust and auditability in proof assistants themselves.