Coq

Reference:

Isabelle advantages over Coq:

From Benjamin Pierce

  • notion of equality is extensional; it eliminates a lot of low-level tedium in proofs of involves equality.
  • a much better story about variable binding; formalizing sth that involves binding variables. nominal data type package.

Coq = Gallina + Tactics

Gallina

Core of the Coq: Gallina, a functional programming language;

Heart of Gallina: typed lambda calculus. - Similar to ML programs. - typed lambda calculus - with dependent types, - also with polymorphic types in the style of ML and Haskell, - also with a built-in inductive definition facility, - So called “The Calculus of Inductive Constructions”.

features (“strage twists from traditional func langs”)

  • All functions are total. It has recursion, but all recursion have to terminate, and it has to be obvious to the Gallina type checker that they do.

Tactics

Doing proof in Coq is “constructing lambda terms of appropriate type”:

  • A proposition is a type,
  • A proof of that proposition is a term of that type, an inhabitant of that type.
Created Jul 15, 2020 // Last Updated Nov 7, 2022

If you could revise
the fundmental principles of
computer system design
to improve security...

... what would you change?