This talk address some of the difficulties of using proof tools in an engineering setting. In particular it focuses on some of the pains engineers face when using proof tools and suggests ways to make the act of proving more palatable.  These suggestions are the basic design decisions for the new Event-B prover tool used in the RODIN platform.