An overview of Cog Xinyu Feng USTC
An overview of Coq Xinyu Feng USTC
What is Cog? A proof assistant developed by INRIA https://coq.inria.fr/ Coq is a formal proof management system.It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs
What is Coq? • A proof assistant developed by INRIA • https://coq.inria.fr/ • Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs …
What is Cog? A functional programming language with rich type sys. Define inductive data types and write algorithms manipulating them. All programs must terminate. A higher-order logic with interactive theorem prover Allows you to reason about mathematical structures and your programs Generates machine-checkable proofs A meta-language/logic Allows you to encode another language/logic and prove the properties of that language/logic
What is Coq? • A functional programming language with rich type sys. • Define inductive data types and write algorithms manipulating them. • All programs must terminate. • A higher-order logic with interactive theorem prover • Allows you to reason about mathematical structures and your programs • Generates machine-checkable proofs • A meta-language/logic • Allows you to encode another language/logic and prove the properties of that language/logic
Why Coq? To have more rigorous formal reasoning For mathematics and program verification Tools like Coq boost program verification
Why Coq? • To have more rigorous formal reasoning • For mathematics and program verification • Tools like Coq boost program verification
Program verification under attack Reports and Articles Social Processes and Proofs of Theorems and Programs [CACM1979] Richard A.De Millo Georgia Institute of Technology Richard J.Lipton and Alan J.Perlis Mathematical proofs can often Yale University be wrong! Program verification Mathematics is trustworthy because of the social process to would never work... check/validate proofs. But nobody would care or check proofs for programs:"The verification of even a puny program can run into dozens of pages,and there's not alight moment or a spark of wit on any of those pages.Nobody is going to run into a friend's office with a program verification...Nobody is ever going to read it
Program verification under attack Program verification would never work … Mathematical proofs can often be wrong! Mathematics is trustworthy because of the social process to check/validate proofs. But nobody would care or check proofs for programs: “The verification of even a puny program can run into dozens of pages, and there's not alight moment or a spark of wit on any of those pages. Nobody is going to run into a friend's office with a program verification … Nobody is ever going to read it.” [CACM 1979]