Z (pronounced "Zed" in this context) is a
language used in
software engineering for
formally describing systems of all kinds, especially
information processing systems, the most common example being
computer programs.
Z is not a programming language. It is much closer to a markup language such as HTML and XML. It describes the system in terms of inputs, outputs and data types. It relies on a lot of math, especially logic, calculus and set theory, with the aim of a Z specification being to produce a description of the system that can be proven mathematically correct: in other words, you can prove that your program will always behave in a way that is precisely defined and totally predictable, if not always the way you wished/designed it to.
Z is a funny language to look at: boxes and lines and strange mathematical-notation arrows for functions, surjections, injections and bijections abound. It looks like math, and as such it cannot be easily typed straight into a computer using an ordinary keyboard. Instead, using backslash as an escape symbol, a variety of codes are used to represent the various mathematical symbols. These can be interpreted by LaTeX to "draw out" a more human-readable version of the specification.
Z cannot be compiled, because it's not a programming language. However, an interpreter called fuzz can be used with LaTeX to perform type checking. However, this simply ensures that the specification is valid Z and that data types are used consistently: the specification could still be wrong or nonsensical.