Formal Methods teaching at undergraduate level has been going on at Manchester for a good number of years.We have introduced various courses based on different approaches.We have experienced the usual problems.To combat these problems, our approaches and our course contents have evolved accordingly over the years. In this paper we briefly trace this evolution, and describe the latest course, on reasoning about simple imperative programs, for first-year students who are half-way through our introductory programming course.