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,
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 and demonstrate
the advances we have made in teaching the above-mentioned concepts
in programming classes.