This week Dr Darbari talks to Prof. Moshe Vardi - one of the best-known names in computing and formal methods. In the first of the two episodes, we trace Moshe's journey from his early years and talk about logic, applications of logic to law, NP-complete problems, ENIAC, John von Neumann, John Backus, compilers, semantics, abstractions, descriptions. Moshe shares fascinating accounts of chat with Ed Clarke and the history of LTL, CTL, SVA and PSL. Find out why model checking works. Thank you very much, Moshe, for taking time out to talk to us.