Modern software systems control a vast portion of our life and are often safety-critical, e.g. it would be catastrophic for an airplane autopilot or a medical device to have a bug. Thus, it is important to ensure that our software works correctly under all possible circumstances. With this goal in mind, this course introduces the well-known interactive proof assistant Coq and relies on it to develop simple ways of applying logical reasoning to programs in order to establish their correctness and safety. This is a hands-on course with 2 mini-project homeworks. Students who do not have the prerequisites but with equivalent background may seek approval from the instructor for enrollment in the course.