Getting it Right

Writing correct programs involves solving two very difficult problems.

  • Saying what you want the program to do.
  • Convincing someone (possibly yourself) that your program does what you say it does.

This course explores some of the fundamental tools that computer science gives us to reason about the correctness of programs. This course is based on my experience teaching the introductory data structures course at Carnegie Mellon. 

The ideas in this course apply to any language; this course avoids focusing on any one programming language; we will write some JavaScript or Python and some code in a peculiar teaching language called C0 (pronounced "see naught") developed at Carnegie Mellon. If you have experience and/or interest in the Java programming language, the course on Contracts and Correctness with JML covers the same ideas with a Java language perspective.


Either the Computation or Change course or some experience writing programs with loops and functions that call each other. 


After this course, you'll be able to answer questions like:

  • How do I prove a program is correct?
  • How do I prove that a program is incorrect?
  • What does partial and total correctness mean?
  • How do we prove correctness of a function with loops and recursive calls?
  • What is a contracts and how do contracts help us prove programs correct?