Join 10350+ others. No spamming.
I promise!

Follow us at github.



david-christiansen / pudding


A language-integrated proof assistant, for and in Racket



Build Status Coverage Status

Pudding is a proof assistant under development at Indiana University, deeply integrated with the Racket programming language.


Pudding is currently incomplete, and cannot yet be used to prove anything. Work is currently being done on the foundations of the proof assistant, such as the representation of refinement rules and the proof mechanisms. When these are ready, we can being the task of encoding a type theory for Racket.

Installation Instructions

Most of Pudding's dependencies are available on the Racket package server. There is one significant exception, which is a library of GUI components which has not yet had an official release.

First, clone the GUI components repository. In the checked-out directory, run:

.../racket-presentation-gui$ raco pkg install -n presentations --deps search-auto

In the above, the $ represents the prompt. Neither it nor the proceeding text should not be typed in.

Once that's done, check out this repository and enter the directory. To install its dependencies, type:

.../pudding$ raco pkg install -n pudding --deps search-auto

To test the GUI, run:

.../pudding$ racket presentation-gui.rkt

To test code generation, run the files in the demo/ subdirectory.

Web Site

The official Pudding Web site is at