Pudding is a new proof assistant under development at Indiana University. Our vision is an extensible system for programming and proving, deeply integrated with a practical programming language.

Diverse Interfaces

(define/pudding identity
    (Isect ([A Type]) (-> A A))
  (intro 'A)
  (intro 'x)
Pudding screenshot

Pudding will support both interactive graphical development and automation through an open tactic API.

Language Integration

Pudding uses Racket for everything:

  • Specifications
  • Proof automation
  • Extracted code
  • Extensions
There is no need to juggle languages when working in Pudding!

The Team

Picture of David Christiansen

David Christiansen

Picture of Tori Lewis

Tori Lewis

Picture of Sam Tobin-Hochstadt

Sam Tobin-Hochstadt

Join us!