I discuss Coq, a widely used proof assistant based on a constructive type theory.  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.