In this chapter we’ll be introducing PlusCal. PlusCal is a language that compiles down to TLA+. Lamport developed it in 2009 to make TLA+ more accessible to programmers. Most of the things we’ll want to do will be significantly easier in PlusCal than in TLA+. This chapter will cover all of PlusCal with the exception of multiprocess algorithms, which is Chapter 5; and fair processes, which is Chapter 6.