Skip to main content

Exam



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) ?