  We present a novel approach for teaching logic and the metatheory of logic to
students who have some experience with functional programming. We define
concepts in logic as a series of functional programs in the language of the
proof assistant Isabelle/HOL. This allows us to make notions which are often
unclear in textbooks precise, to experiment with definitions by executing them,
and to prove metatheoretical theorems in full detail. We have surveyed student
perceptions of our teaching approach to determine its usefulness and found that
students felt that our formalizations helped them understand concepts in logic,
and that they experimented with them as a learning tool. However, the approach
was not enough to make students feel confident in their abilities to design and
implement their own formal systems. Further studies are needed to confirm and
generalize the results of our survey, but our initial results seem promising.
