demoness101, which is shaping up to be a fantastic book. It's a bit disturbing to hear the same general ideas being spoken so long ago, and to realize they still haven't "won", but I guess a lot of particular progress has been made. Nonetheless, the whole endeavour of mechanical reasoning about mechanical systems needs to put its money and code where its mouth is pretty damn soon.Frank is talking a bit in class about the stuff
kitty_tape was working on last summer, with focusing and checking proofs in a format more human-friendly than λ-calculus terms. Also some neat stuff about abstract congruence closure algorithms. I need to go back and look at Mizar again.