proust An implementation of Prabhakar Ragde's proust proof assistant following Logic and Computation Intertwined