Formal meaning of programs. Three classical styles: operational (how it runs, step-by-step), denotational (what mathematical object it denotes), axiomatic (which logical properties hold).