Formal specification -- contracts

• type specification -- local properties
• relational specification -- structural properties, type relations
• functional specification -- requirements

Verification -- as a design methodology

• reasoning about program specification/code

Runtime consistency -- invariance

• behavioral types specify test cases
• invariants and assertions monitor consistency