interactive-way-to-c Learning C program proving using Emacs --reminiscent of Coq proving with Proof General.