Skip to main content


Question 1

What is returned by the execution of a smart contract ?

Question 2

What makes the bridge between the Tezos world and the formal world of Coq ?

Question 3

Who is Thierry Coquand ?

Question 4

We have seen that a Michelson script must be translated into an annotated script (i.e. a formal definition) (because Mi-Cho-Coq provides an equivalent for each Michelson instruction). In the theorem we want to prove, we specify that "the execution of the annotated script is equivalent to post-conditions". Who is responsible for the execution of this annotated script ?

Question 5

What post-conditions depends on (What post-conditions are built upon) ?