Tutch

Tutch is short for tutorial proof checker, and was initially designed and implemented in Standard ML by Andreas Abel for use in education.

I believed that a web application could improve upon the feedback cycle offered by a command line application. A command line utility requires switching contexts to the command line and then lining up the command line output with what was written in a separate editor. In contrast, my “retutch” implementation could give near-instantaneous feedback on which assertions are supported by the rules of constructive first-order logic.

An interesting constraint was that, while I felt the surface syntax of Tutch could be improved substantially, I did not allow any changes so that existing documentation and examples would still be a valid guide for the web implementation.

My spouse Chris Martens validated the web implementation, using it for required assignments in the Computational Applied Logic course at NCSU in Fall 2019. While we did not conduct a formal assessment, informally the results were remarkable in their mundanity: students completed several course assignments in Tutch without much trouble or specific instruction in Tutch. Given that the usual documented experience of mechanized proof in university courses is characterized by frustration and difficulty, I consider our experiment quite successful.