Regarding your "serious context of use" thread, have you run across Pierce's "Software Foundations"? It's a "book" which the user progresses through with a proof assistant (e.g. Emacs + Proof General) by writing proofs in Coq. Do recommend. softwarefoundations.cis.upenn.edu
