I've been getting some really good feedback from my series of diary entries on formal proof systems. The latest batch are from Norm Megill (of Metamath fame) and Joe Hurd, who's done quite a bit of work with HOL.
I've used up almost all of my diary time responding to these threads (privately), but the juicy bits will find their way back here.