Arguably, one of the greatest intellectual achievements of Computer Science is the axiomatic reasoning for imperative programs developed by Tony Hoare known as Hoare Logic. This intellectual milestone was developed leaning on historical developments in the field and has profoundly influenced how programs are developed and is used in modern mechanized logic. Therefore, it is surprising that Hoare Logic plays all but a small role in most undergraduate Computer Science curriculums. Usually, Hoare Logic is relegated to an advanced course in Programming Languages or in Program Verification. This is unfortunate given that Hoare Logic and formal methods thinking can be directly used to design programs as demonstrated by Hoare, Dijkstra, Gries, and others. This article puts forth an approach to address this curriculum shortcoming. Instead of relegating Hoare Logic to an advanced course, Hoare Logic can be introduced throughout the undergraduate curriculum. In this manner, the long term hope is to cause a cultural change within the Computer Science community to become more embracing of formal methods thinking.

Dr. Marco T. Morazán joined Seton Hall in 1999. He did his undergraduate studies at Rutgers University and his graduate work at the City University of New York. At Seton Hall he teaches at all levels of the Computer Science curriculum including his signature courses: Introduction to Program Design I and II, Organization of Programming Languages, and Automata Theory and Computability. His main research foci are the implementation of programming languages, functional programming, and Computer Science Education. He is responsible for an optimal lambda lifting algorithm and an effective mechanism for closure memoization. In Computer Science education, he is especially proud of the effectiveness of the Computer Science curriculum, based on the development of video games, he has developed for beginners.