https://jsiek.github.io/deduce/index.html

A proof checker meant for education

Teaching correctness proofs of functional programs to students.

Get Started Live Code
Deduce hippo logo

What is Deduce?

Deduce is an automated proof checker meant for use in education to
help students:

  * Ease their way into proving the correctness of programs.
  * Deepening their understanding of logic.
  * Improve their ability to write mathematical proofs.

Who can use Deduce?

The intended audience is students with (roughly) the following
background knowledge and skills:

  * Basic programming skills in a mainstream language such as Java,
    Python, or C++
  * Some exposure to logic, as one would learn in a course on
    Discrete Mathematics

Get Started

Get started by installing the necessary prerequisites and downloading
the Deduce source code.

You can also find handy information on setting up your Deduce
workspace.

Get Started

Write Deduce Code

Go through a series of examples to familiarize yourself with Deduce
functional programming.

Check your understanding with exercises to test your knowledge of the
language.

Start Programming

Prove Your Programs

Follow a detailed tutorial to learn how to write logical proofs using
Deduce effectively.

Explore all of the features of the Deduce proof language in this
comprehensive guide.

Start Proving

Need Help?

The Deduce Reference manual provides an alphabetical list of all the
features in Deduce.

The Cheat Sheet gives some advice regarding proof strategy and which
Deduce keyword to use next in a proof.

Reference Manual Cheat Sheet

Example Proof

As a taster for what it looks like to write programs and proofs in
Deduce, the following is an implementation of the Linear Search
algorithm and a proof that item y does not occur in the list xs at a
position before the index returned by search(xs, y)


Credits

This open-source software is brought to you by the volunteer work of
the following people.

  * Matei Cloteaux
  * Shulin Gonsalves
  * Calvin Josenhans
  * Jeremy Siek