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.
(define/pudding identity (Isect ([A Type]) (-> A A)) (intro 'A) (intro 'x) (auto))
Pudding will support both interactive graphical development and automation through an open tactic API.
Pudding uses Racket for everything: