Trustworthy Formal Natural Language Specifications

Explore a groundbreaking approach to bridging the gap between natural language specifications and formal verification in this 30-minute conference talk from Onward! 2023. Delve into the innovative work of Colin S. Gordon and Sergey Matskevich from Drexel University as they present a method for creating trustworthy formal natural language specifications within existing proof assistants. Learn how their implementation allows for specifications to be written in expressive subsets of English, automatically translated into formal claims, and verified within the Lean proof assistant. Discover the extensible and modular nature of their approach, which produces proof certificates explaining word interpretation and sentence structure computation. Examine the practical application of this prototype in translating English descriptions of formal specifications from a popular textbook into Lean formalizations. Gain insights into the potential impact of this research on improving the accuracy and efficiency of software verification processes.