Danvy introduced the concept of “mystery functions” as a way to teach multiple programming-related concepts that are often treated separately in common computer science curricula, in particular, specification, implementation, testing, recursion and induction. He presented concepts using the Rocq Prover. As part of a course on software correctness, we have recast Danvy’s pedagogical themes using Slang, a verification-enabled subset of the Scala programming language, and its companion verification tool Logika. Together, Slang and Logika allow developers to program in a rich programming language and apply a variety of specification and verification techniques, including method contracts, SMT-based automated reasoning, and semi-automated proofs in Logika’s proof language that includes natural deduction, induction, and term-rewriting – all phrased in directly in Scala/Slang syntax that is easily accessible to programmers. This synergistic combination of programming and proof features enables us to convincingly encourage students with the mantras that “doing proofs is programming” (and vice versa). As we teach concepts using Danvy’s “mystery function” with Slang/Logika in a full programming language that blends programs and proofs, we add another dimension to the students’ learning. In this paper we describe mystery functions in Slang demonstrating the advances we have made in teaching the above-mentioned concepts in programming classes.