Now, my former W3C colleague Dan Connolly pointed out to me a long, long time ago that one can use specification languages like Alloy not just to check software designs, but to test our understanding of things we read. Dan told me once that when he really wanted to understand something, he tried to model it using a specification language and prove at least a few trivial theorems about it.
One reason I love Alloy