I've been reading several books by mathematician programmers (Donal Knuth, Alexander Stepanov, Edsger Dijkstra), and one book about UML. TLA+ does what UML is supposed to: provide a solid foundation for designing and reasoning about programs. TLA+ is also designed to be typeset a la TeX and fed into validation programs. Unfortunately, I'm not a big fan of the ASCII representation.

Book's website (including errate, tools, and PDF version of book) is at http://www.tlaplus.net/documentation/... .

Disclaimer: I've chickened out after getting to Advanced section. Lamport is at galaxy brain level with math.

But first section is great. It provided an awesome example how you can start with a basic toy spec and refine it until you get something useful and real.
This was very enlightening.

First few chapters are interesting mathematics (called temporal logic) and later goes on to explain concurrency and sequential consistency. Later half of the book requires the supplementary material from author's website.