Teaching Functional Programmers Logic and Metatheory

TL;DR

This paper introduces a novel method for teaching logic and metatheory to students with functional programming experience by using proof assistant Isabelle/HOL to define, experiment with, and prove logical concepts.

Contribution

It presents a new approach that formalizes logic concepts as functional programs in Isabelle/HOL, enhancing understanding and experimentation in logic education.

Findings

Students found formalizations helpful for understanding logic concepts.

Students used the formalizations as a learning tool for experimentation.

The approach did not fully boost students' confidence in designing formal systems.

Abstract

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.