This page collects resources for anyone considering the use of formal methods and formal tools in a classroom. The effort grew out of a discussion that was held during the Big Proof program at the Isaac Newton Institute in Cambridge, UK. A recording of the discussion is available.

There are many axes along which one can organize such a list, such as the level of expertise of the intended audience (from experts to the public at large) or disciplinary orientation (computer science, mathematics, mathematical logic, etc.). Here I have chosen to classify the material by subject matter:

  • computer science: material for teaching students to use formal methods for computational purposes, e.g. courses on software design and verification.

  • mathematics: material for teaching mathematics, e.g. courses on discrete mathematics or introductions to mathematical proof.

  • logic and formal methods: materials for teaching logic and formal methods themselves, e.g. courses on dependent type theory and automated reasoning.

If you would like add something, just send the text as you would like it to appear to avigad@cmu.edu, preferrably already formatted in markdown. Entries should provide a link to the relevant resources, which in turn should make use of formal tools (theorem provers, SAT solvers, model checkers, etc.) in some way.

Computer Science

Mathematics

  • Jeremy Avigad, Robert Y. Lewis, and Floris van Doorn, Logic and Proof

    An introduction to mathematical proof and symbolic logic, with exercises in Lean.

  • Daniel Velleman, Proof Designer

    A Java applet designed to help students write proofs.

  • The STACK Project

    A system for designing sophisticated computer-aided assessments in mathematics.

  • Chris Sangwin, Computer Aided Assessment of Mathematics

    A book on the use of computer aided assessment.

Logic and Formal Methods