Along with type systems, I'm casually interested in formal specifications and verification of software.  During lunch today, I watched an internal Microsoft Research talk given by Leslie Lamport.  The topic was TLA+ -- his formal verification system -- during which he blurted out a couple amusing quotes:

"Writing is nature's way of letting you know how sloppy your thinking is."
       --- Guindon (cartoon)

"Math is nature's way of letting you know how sloppy your writing is."
       --- Leslie Lamport (riffing on Guindon)

And related:

"Formal math is nature's way of letting you know how sloppy your math is."
       --- Leslie Lamport

They made me chuckle out loud, so I figured I'd share them.  Unfortunately the talk isn't available outside the company (as far as I can tell), but Lamport has written a book, Specifying Systems, available online, in addition to dozens of interesting papers, on the topic.