The Coq Proof Assistant

Published: Dec. 29, 2021, 4 a.m.

b'

I discuss Coq, a widely used proof assistant based on a constructive type theory.\\xa0 One episode definitely cannot do justice to the complexity of a tool like this -- but I take a first try at covering its features at a high level.

'