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.
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
The official Pudding Web site is at http://pudding-prover.org.