В первой части мы обсудим формальные доказательства и Coq в общем, разберемся для чего он нужен, где применяется, его место среди других инструментов формальной верификации, затронем экосистему Coq, а также рассмотрим методы связи верифицированных программ и исполняемого кода, такие как экстракция и эмбединг. Во второй части посмотрим на многочисленных примерах на особенности Coq как языка программирования. В процессе обсудим слабую/сильную нормализацию, зависимые типы, тактики, тотальность, строгую позитивность, иерархию вселенных типов, непредикативность, различия между Type и Prop, экстракцию.