We relate our approach to teaching a unit in Dafny on programming language basics and security properties like non-interference. This unit is part of a broader course on building secure software systems. The course targets primarily Masters students with little or no background in PL. We show how relating the PL concepts to concrete Dafny representations helps ground the concepts for students. We also describe a series of carefully scaffolded assignments that build to the point where the students, in the context of a simplified C-like language, prove type safety, non-interference for a security type system, and non-interference for a dynamic taint tracker. Finally, we share lessons learned from four offerings of this Dafny-based unit.