Calculational Proofs in ACL2s

TL;DR

This paper presents a mechanically-checkable calculational proof system integrated into ACL2s, designed to teach formal reasoning to undergraduates, with automated correctness checking and educational feedback.

Contribution

It introduces a novel calculational proof checker in ACL2s, tailored for educational use, with a user-friendly interface and practical teaching applications.

Findings

Successfully taught over a thousand students using the proof system

Proof checker provides automatic correctness verification and feedback

The system is integrated into multiple platforms including Eclipse and web

Abstract

Teaching college students how to write rigorous proofs is a critical objective in courses that introduce formal reasoning. Over the course of several years, we have developed a mechanically-checkable style of calculational reasoning that we used to teach over a thousand freshman-level undergraduate students how to reason about computation in our "Logic and Computation" class at Northeastern University. We were inspired by Dijkstra, who advocated the use of calculational proofs, writing "calculational proofs are almost always more effective than all informal alternatives, ..., the design of calculational proofs seems much more teachable than the elusive art of discovering an informal proof." Our calculational proof checker is integrated into ACL2s and is available as an Eclipse IDE plugin, via a Web interface, and as a stand-alone tool. It automatically checks proofs for correctness and provides useful feedback. We describe the architecture of the checker, its proof format, its underlying algorithms, its correctness and provide examples using proofs from our undergraduate class and from Dijkstra. We also describe our experiences using the proof checker to teach undergraduates how to formally reason about computation.