I always wondered about dependent types. Even though it was a little bit too technical for me, at least I have some idea about what it really is.

By the way, Z notation rocks.