The standard joke about my university's grad-level programming languages course is that its formalization unit does a great job of identifying undergrads by discussing Peano naturals and Hoare logic in the same lecture...